def Equipotent (α : Type u) (β : Type v) : Prop

Equations

• Equipotent α β = Nonempty (Function.Bijection α β)

theorem Equipotent.symm {α : Type u_1} {β : Type u_2} (h : Equipotent α β) : Equipotent β α

theorem Equipotent.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : Equipotent α β) (h' : Equipotent β γ) : Equipotent α γ

theorem Equipotent.of_eq {α β : Type u} (h : α = β) : Equipotent α β

def equipotent_rel : Relation (Type u) (Type u)

Equations

• equipotent_rel (α, β) = Nonempty (Function.Bijection α β)

@[simp]

theorem mem_equipotent_rel_iff {α β : Type u} : (α, β) ∈ equipotent_rel ↔ Equipotent α β

instance instEquivalenceEquipotent : Equivalence Equipotent

Equations

• instEquivalenceEquipotent = ⋯

instance equipotent_equiv : equipotent_rel.IsEquivalence

Equations

• equipotent_equiv = ⋯

def Cardinal : Type (u + 1)

Equations

• Cardinal = Quot Equipotent

def Cardinal.mk : Type u_1 → Cardinal

Equations

• Cardinal.mk = Quot.mk Equipotent

@[simp]

theorem Cardinal.mk_surj : Function.Surjective Cardinal.mk

theorem Cardinal.alt : Cardinal = Quot (Function.curry equipotent_rel)

theorem Cardinal.mk_alt {α : Type u} : Cardinal.mk α = Quot.mk (Function.curry equipotent_rel) α

@[simp]

theorem Cardinal.eq_iff {α β : Type u} : Cardinal.mk α = Cardinal.mk β ↔ Equipotent α β

instance instZeroCardinal : Zero Cardinal

Equations

• instZeroCardinal = { zero := Cardinal.mk PEmpty }

instance instOneCardinal : One Cardinal

Equations

• instOneCardinal = { one := Cardinal.mk PUnit }

theorem Cardinal.zero_eq : 0 = Cardinal.mk PEmpty

theorem Cardinal.one_eq : 1 = Cardinal.mk PUnit

@[simp]

theorem Cardinal.eq_zero_iff {α : Type u} : Cardinal.mk α = 0 ↔ α → False

@[simp]

theorem Cardinal.eq_one_iff {α : Type u} : Cardinal.mk α = 1 ↔ Nonempty (Unique α)

@[simp]

theorem Cardinal.zero_neq_one : 0 ≠ 1

theorem Cardinal.le_equipotent_invariant1 {x x' y y' : Type u} (hx : Equipotent x x') (hy : Equipotent y y') (h : Nonempty (Function.Injection x y)) : Nonempty (Function.Injection x' y')

theorem Cardinal.le_equipotent_invariant {x x' y y' : Type u} (hx : Equipotent x x') (hy : Equipotent y y') : Nonempty (Function.Injection x y) = Nonempty (Function.Injection x' y')

def Cardinal.injects (α β : Cardinal) : Prop

Equations

• α.injects β = Quot.lift2_same (fun (α β : Type ?u.3) => Nonempty (Function.Injection α β)) ⋯ α β

@[simp]

theorem Cardinal.mk_injects_iff {α β : Type u} : (Cardinal.mk α).injects (Cardinal.mk β) ↔ Nonempty (Function.Injection α β)

@[simp]

theorem Cardinal.mk_injects_iff' {α β : Type u} : Cardinal.injects (Quot.mk Equipotent α) (Quot.mk Equipotent β) ↔ Nonempty (Function.Injection α β)

instance instPreorderCardinal : Preorder Cardinal

Equations

• instPreorderCardinal = Preorder.mk instPreorderCardinal.proof_1 instPreorderCardinal.proof_2 instPreorderCardinal.proof_3

@[simp]

theorem Cardinal.mk_le_iff {α β : Type u} : Cardinal.mk α ≤ Cardinal.mk β ↔ Nonempty (Function.Injection α β)

@[simp]

theorem Cardinal.zero_le (x : Cardinal) : 0 ≤ x

theorem Cardinal.one_le_iff_neq_zero {x : Cardinal} : 1 ≤ x ↔ x ≠ 0

theorem Cardinal.factors_through_mk {α : Type v} {f : α → Cardinal} : ∃ (g : α → Type u), f = Cardinal.mk ∘ g

def Cardinal.ind_mk {p : Cardinal → Prop} (h : ∀ (α : Type u), p (Cardinal.mk α)) (x : Cardinal) : p x

Equations

• ⋯ = ⋯

noncomputable instance instWellOrderCardinal : WellOrder Cardinal

Equations

• instWellOrderCardinal = ⋯.wellOrder

theorem cantor_bernstein_schroeder {α β : Type u} (f : Function.Injection α β) (g : Function.Injection β α) : Equipotent α β

theorem exists_injection {α β : Type u} : (∃ (f : α → β), Function.Injective f) ∨ ∃ (f : β → α), Function.Injective f

def Cardinal.sigma {ι : Type u} (α : ι → Cardinal) : Cardinal

Equations

• Cardinal.sigma α = Cardinal.mk (let b := fun (i : ι) => Classical.choose ⋯; (i : ι) × b i)

def Cardinal.prod {ι : Type u} (α : ι → Cardinal) : Cardinal

Equations

• Cardinal.prod α = Cardinal.mk (let b := fun (i : ι) => Classical.choose ⋯; (i : ι) → b i)

@[simp]

theorem Cardinal.sigma_mk {ι : Type u} {α : ι → Type u} : (Cardinal.sigma fun (i : ι) => Cardinal.mk (α i)) = Cardinal.mk ((i : ι) × α i)

@[simp]

theorem Cardinal.prod_mk {ι : Type u} {α : ι → Type u} : (Cardinal.prod fun (i : ι) => Cardinal.mk (α i)) = Cardinal.mk ((i : ι) → α i)

theorem Cardinal.sigma_ub {ι : Type u} {α : ι → Cardinal} : UpperBound (α '' Set.univ) (Cardinal.sigma α)

theorem Cardinal.exists_lubi {ι : Type u} {α : ι → Cardinal} : ∃ (x : Cardinal), IsLUBi α x

theorem Cardinal.ge_of_surj {α β : Type u} (h : Function.Surjection α β) : Cardinal.mk β ≤ Cardinal.mk α

theorem Cardinal.iUnion_le_sigma {ι β : Type u} {α : ι → Set β} : Cardinal.mk ↥(⋃ i : ι, α i) ≤ Cardinal.sigma fun (i : ι) => Cardinal.mk ↥(α i)

theorem Cardinal.sigma_reindex {ι ι' : Type u} {α : ι → Cardinal} (f : Function.Bijection ι' ι) : Cardinal.sigma (α ∘ f.val) = Cardinal.sigma α

theorem Cardinal.sigma_reindex_univ {ι : Type u} {α : ι → Cardinal} : (Cardinal.sigma fun (x : ↥Set.univ) => match x with | ⟨x, property⟩ => α x) = Cardinal.sigma α

theorem Cardinal.prod_reindex {ι ι' : Type u} {α : ι → Cardinal} (f : Function.Bijection ι' ι) : Cardinal.prod (α ∘ f.val) = Cardinal.prod α

theorem Cardinal.prod_reindex_univ {ι : Type u} {α : ι → Cardinal} : (Cardinal.prod fun (x : ↥Set.univ) => match x with | ⟨x, property⟩ => α x) = Cardinal.prod α

theorem Cardinal.prod_assoc {ι ι' : Type u} {α : ι → Cardinal} {p : ι' → Set ι} (h : Set.IsPartition p) : Cardinal.prod α = Cardinal.prod fun (i' : ι') => Cardinal.prod fun (i : ↥(p i')) => α i.val

theorem Cardinal.sigma_assoc {ι ι' : Type u} {α : ι → Cardinal} {p : ι' → Set ι} (h : Set.IsPartition p) : Cardinal.sigma α = Cardinal.sigma fun (i' : ι') => Cardinal.sigma fun (i : ↥(p i')) => α i.val

theorem Cardinal.sigma_prod_distrib {ι : Type u} {ι' : ι → Type u} {x : (i : ι) → ι' i → Cardinal} : (Cardinal.prod fun (i : ι) => Cardinal.sigma fun (i' : ι' i) => x i i') = Cardinal.sigma fun (y : (i : ι) → ι' i) => Cardinal.prod fun (i : ι) => x i (y i)

instance instAddCardinal : Add Cardinal

Equations

• instAddCardinal = { add := fun (x y : Cardinal) => Cardinal.mk (⋯.choose ⊕ ⋯.choose) }

instance instMulCardinal : Mul Cardinal

Equations

• instMulCardinal = { mul := fun (x y : Cardinal) => Cardinal.mk (⋯.choose × ⋯.choose) }

instance instPowCardinal : Pow Cardinal Cardinal

Equations

• instPowCardinal = { pow := fun (x y : Cardinal) => Cardinal.mk (⋯.choose → ⋯.choose) }

@[simp]

theorem Cardinal.add_mk {α β : Type u} : Cardinal.mk α + Cardinal.mk β = Cardinal.mk (α ⊕ β)

@[simp]

theorem Cardinal.mul_mk {α β : Type u} : Cardinal.mk α * Cardinal.mk β = Cardinal.mk (α × β)

@[simp]

theorem Cardinal.pow_mk {α β : Type u} : Cardinal.mk α ^ Cardinal.mk β = Cardinal.mk (β → α)

theorem Cardinal.add_comm {a b : Cardinal} : a + b = b + a

theorem Cardinal.mul_comm {a b : Cardinal} : a * b = b * a

@[simp]

theorem Cardinal.add_assoc {a b c : Cardinal} : a + (b + c) = a + b + c

@[simp]

theorem Cardinal.mul_assoc {a b c : Cardinal} : a * (b * c) = a * b * c

theorem Cardinal.mul_add_distrib_right {a b c : Cardinal} : (a + b) * c = a * c + b * c

theorem Cardinal.mul_add_distrib_left {a b c : Cardinal} : a * (b + c) = a * b + a * c

theorem Cardinal.sigma_zeros {ι : Type u} {α : ι → Cardinal} {s : Set ι} (h : ∀ (x : ι), ¬x ∈ s → α x = 0) : Cardinal.sigma α = Cardinal.sigma fun (x : ↥s) => α x.val

theorem Cardinal.prod_ones {ι : Type u} {α : ι → Cardinal} {s : Set ι} (h : ∀ (x : ι), ¬x ∈ s → α x = 1) : Cardinal.prod α = Cardinal.prod fun (x : ↥s) => α x.val

@[simp]

theorem Cardinal.add_zero {a : Cardinal} : a + 0 = a

@[simp]

theorem Cardinal.zero_add {a : Cardinal} : 0 + a = a

@[simp]

theorem Cardinal.mul_one {a : Cardinal} : a * 1 = a

@[simp]

theorem Cardinal.one_mul {a : Cardinal} : 1 * a = a

@[simp]

theorem Cardinal.sigma_constant {α : Type u} {b : Cardinal} : (Cardinal.sigma fun (x : α) => b) = Cardinal.mk α * b

@[simp]

theorem Cardinal.prod_constant {α : Type u} {b : Cardinal} : (Cardinal.prod fun (x : α) => b) = b ^ Cardinal.mk α

@[simp]

theorem Cardinal.sigma_constant_one {α : Type u} : (Cardinal.sigma fun (x : α) => 1) = Cardinal.mk α

@[simp]

theorem Cardinal.prod_zero_iff {ι : Type u} {x : ι → Cardinal} : Cardinal.prod x = 0 ↔ ∃ (i : ι), x i = 0

@[simp]

theorem Cardinal.sigma_zero_iff {ι : Type u} {x : ι → Cardinal} : Cardinal.sigma x = 0 ↔ ∀ (i : ι), x i = 0

theorem Cardinal.sigma_empty {ι : Type u} {x : ι → Cardinal} (h : ι → False) : Cardinal.sigma x = 0

theorem Cardinal.prod_empty {ι : Type u} {x : ι → Cardinal} (h : ι → False) : Cardinal.prod x = 1

theorem Cardinal.sigma_add {a b : Cardinal} : Cardinal.sigma (Sum.elim (fun (x : PUnit) => a) fun (x : PUnit) => b) = a + b

theorem Cardinal.prod_mul {a b : Cardinal} : Cardinal.prod (Sum.elim (fun (x : PUnit) => a) fun (x : PUnit) => b) = a * b

@[simp]

theorem Cardinal.mul_zero {a : Cardinal} : a * 0 = 0

@[simp]

theorem Cardinal.zero_mul {a : Cardinal} : 0 * a = 0

theorem Cardinal.zero_of_mul_zero {a b : Cardinal} (h : a * b = 0) : a = 0 ∨ b = 0

@[simp]

theorem Cardinal.mul_zero_iff {a b : Cardinal} : a * b = 0 ↔ a = 0 ∨ b = 0

@[simp]

theorem Cardinal.add_zero_iff {a b : Cardinal} : a + b = 0 ↔ a = 0 ∧ b = 0

theorem Cardinal.add_one_cancel {a b : Cardinal} (h : a + 1 = b + 1) : a = b

@[simp]

theorem Cardinal.pow_sigma {ι : Type u} {x : ι → Cardinal} {a : Cardinal} : a ^ Cardinal.sigma x = Cardinal.prod fun (i : ι) => a ^ x i

@[simp]

theorem Cardinal.prod_pow {ι : Type u} {x : ι → Cardinal} {a : Cardinal} : Cardinal.prod x ^ a = Cardinal.prod fun (i : ι) => x i ^ a

theorem Cardinal.pow_add {a b c : Cardinal} : a ^ (b + c) = a ^ b * a ^ c

theorem Cardinal.pow_mul {a b c : Cardinal} : a ^ (b * c) = (a ^ b) ^ c

@[simp]

theorem Cardinal.pow_zero {a : Cardinal} : a ^ 0 = 1

@[simp]

theorem Cardinal.pow_one {a : Cardinal} : a ^ 1 = a

@[simp]

theorem Cardinal.one_pow {a : Cardinal} : 1 ^ a = 1

@[simp]

theorem Cardinal.zero_pow_neq_zero {a : Cardinal} (h : a ≠ 0) : 0 ^ a = 0

theorem Cardinal.set_eq_two_pow {α : Type u} : Cardinal.mk (Set α) = (1 + 1) ^ Cardinal.mk α

theorem Cardinal.exists_add_iff_le {a b : Cardinal} : (∃ (c : Cardinal), b = a + c) ↔ a ≤ b

theorem Cardinal.sigma_le {ι : Type u} {x y : ι → Cardinal} (h : ∀ (i : ι), x i ≤ y i) : Cardinal.sigma x ≤ Cardinal.sigma y

theorem Cardinal.prod_le {ι : Type u} {x y : ι → Cardinal} (h : ∀ (i : ι), x i ≤ y i) : Cardinal.prod x ≤ Cardinal.prod y

theorem Cardinal.sigma_subset {ι : Type u} {x : ι → Cardinal} {s : Set ι} : (Cardinal.sigma fun (a : ↥s) => x a.val) ≤ Cardinal.sigma x

theorem Cardinal.prod_subset {ι : Type u} {x : ι → Cardinal} {s : Set ι} (h : ∀ (i : ι), ¬i ∈ s → x i ≠ 0) : (Cardinal.prod fun (a : ↥s) => x a.val) ≤ Cardinal.prod x

theorem Cardinal.add_mono_left {a : Cardinal} : Monotone fun (b : Cardinal) => a + b

theorem Cardinal.add_mono_right {b : Cardinal} : Monotone fun (a : Cardinal) => a + b

theorem Cardinal.mul_mono_left {a : Cardinal} : Monotone fun (b : Cardinal) => a * b

theorem Cardinal.mul_mono_right {b : Cardinal} : Monotone fun (a : Cardinal) => a * b

theorem Cardinal.pow_mono_right {b : Cardinal} : Monotone fun (a : Cardinal) => a ^ b

theorem Cardinal.pow_mono_left {a : Cardinal} (h : a ≠ 0) : Monotone fun (b : Cardinal) => a ^ b

theorem Cardinal.cantor {a : Cardinal} : a < (1 + 1) ^ a

theorem Cardinal.higher_universe {α : Type u} : ¬Equipotent α Cardinal

@[simp]

theorem Cardinal.add_one_neq_zero {a : Cardinal} : a + 1 ≠ 0

@[simp]

theorem Cardinal.le_add_left {a b : Cardinal} : a ≤ a + b

@[simp]

theorem Cardinal.le_add_right {a b : Cardinal} : b ≤ a + b

@[simp]

theorem Cardinal.mk_le_of_subset {α : Type u_1} {x y : Set α} (h : x ⊆ y) : Cardinal.mk ↥x ≤ Cardinal.mk ↥y

theorem Cardinal.preimage_same_product {α β : Type u} {f : α → β} {c : Cardinal} (h' : ∀ (y : β), Cardinal.mk ↥(f ⁻¹' {y}) = c) : Cardinal.mk α = c * Cardinal.mk β

theorem Equipotent.subset_subset {α : Type u} {s t : Set α} (h : s ⊆ t) : Equipotent ↥{x : ↥t | x.val ∈ s} ↥s

theorem Cardinal.disj_iUnion {α ι : Type u} {a : ι → Set α} (h : Set.Disjoint a) : Cardinal.mk ↥(⋃ i : ι, a i) = Cardinal.sigma fun (i : ι) => Cardinal.mk ↥(a i)

theorem Cardinal.mk_diag {α : Type u} : Cardinal.mk α = Cardinal.mk ↥Relation.diag