Common.Set.Finite

Additional theorems around finite sets.

Definitions

def Set.Equinumerous {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : Prop

A set A is equinumerous to a set B (written A ≈ B) if and only if there is a one-to-one function from A onto B.

Equations

• (A ≈ B) = ∃ (F : α → β), Set.BijOn F A B

def Set.«term_≈_» : Lean.TrailingParserDescr

Equations

• Set.«term_≈_» = Lean.ParserDescr.trailingNode `Set.term_≈_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 51))

theorem Set.equinumerous_def {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : A ≈ B ↔ ∃ (F : α → β), Set.BijOn F A B

def Set.NotEquinumerous {α : Type u_1} {β : Type u_2} (A : Set α) (B : Set β) : Prop

A set A is not equinumerous to a set B (written A ≉ B) if and only if there is no one-to-one function from A onto B.

Equations

• (A ≉ B) = ¬A ≈ B

def Set.«term_≉_» : Lean.TrailingParserDescr

Equations

• Set.«term_≉_» = Lean.ParserDescr.trailingNode `Set.term_≉_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≉ ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Set.not_equinumerous_def : ∀ {α : Type u_1} {A : Set α} {α_1 : Type u_2} {B : Set α_1}, A ≉ B ↔ ∀ (F : α → α_1), ¬Set.BijOn F A B

theorem Set.equinumerous_refl {α : Type u_1} (A : Set α) : A ≈ A

For any set A, A ≈ A.

theorem Set.equinumerous_symm {α : Type u_1} {β : Type u_2} [Nonempty α] {A : Set α} {B : Set β} (h : A ≈ B) : B ≈ A

For any sets A and B, if A ≈ B. then B ≈ A.

theorem Set.equinumerous_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {A : Set α} {B : Set β} {C : Set γ} (h₁ : A ≈ B) (h₂ : B ≈ C) : ∃ (H : α → γ), Set.BijOn H A C

For any sets A, B, and C, if A ≈ B and B ≈ C, then A ≈ C.

theorem Set.eq_imp_equinumerous {α : Type u_1} {A : Set α} {B : Set α} (h : A = B) : A ≈ B

If two sets are equal, they are trivially equinumerous.

Finite Sets

axiom Set.finite_iff_equinumerous_nat {α : Type u_1} {S : Set α} : Set.Finite S ↔ ∃ (n : ℕ), S ≈ Set.Iio n

A set is finite if and only if it is equinumerous to a natural number.

Emptyset

@[simp]

theorem Set.equinumerous_zero_iff_emptyset {α : Type u_1} {S : Set α} : S ≈ Set.Iio 0 ↔ S = ∅

Any set equinumerous to the emptyset is the emptyset.

theorem Set.equinumerous_emptyset_emptyset {β : Type u_1} {α : Type u_2} [Bot β] : ∅ ≈ ∅

Empty sets are always equinumerous, regardless of their underlying type.

theorem Set.succ_diff_succ_equinumerous_diff {m : ℕ} {n : ℕ} : Set.Iio (Nat.succ m) \ Set.Iio (Nat.succ n) ≈ Set.Iio m \ Set.Iio n

For all natural numbers m, n, m⁺ - n⁺ ≈ m - n.

theorem Set.diff_union_equinumerous_succ_diff {m : ℕ} {n : ℕ} (hn : n ≤ m) : Set.Iio m \ Set.Iio n ∪ {m} ≈ Set.Iio (Nat.succ m) \ Set.Iio n

For all natural numbers m, n, m - n ∪ {m} ≈ m - n.