Cardinal Numbers

We define cardinal numbers as a quotient of types under the equivalence relation of equinumerosity (i.e., existence of a bijection).

Main definitions

• Cardinal is the type of cardinal numbers (in a given universe).
• Cardinal.mk α or #α is the cardinality of α. The notation # lives in the locale Cardinal.
• Addition c₁ + c₂ is defined by Cardinal.add_def α β : #α + #β = #(α ⊕ β).
• Multiplication c₁ * c₂ is defined by Cardinal.mul_def : #α * #β = #(α × β).
• Exponentiation c₁ ^ c₂ is defined by Cardinal.power_def α β : #α ^ #β = #(β → α).
• Cardinal.sum is the sum of an indexed family of cardinals, i.e. the cardinality of the corresponding sigma type.
• Cardinal.prod is the product of an indexed family of cardinals, i.e. the cardinality of the corresponding pi type.
• Cardinal.aleph0 or ℵ₀ is the cardinality of ℕ. This definition is universe polymorphic: Cardinal.aleph0.{u} : Cardinal.{u} (contrast with ℕ : Type, which lives in a specific universe). In some cases the universe level has to be given explicitly.

Implementation notes

• There is a type of cardinal numbers in every universe level: Cardinal.{u} : Type (u + 1) is the quotient of types in Type u. The operation Cardinal.lift lifts cardinal numbers to a higher level.
• Cardinal arithmetic specifically for infinite cardinals (like κ * κ = κ) is in the file Mathlib/SetTheory/Cardinal/Ordinal.lean.

References

• https://en.wikipedia.org/wiki/Cardinal_number

Tags

cardinal number, cardinal arithmetic, cardinal exponentiation, aleph, Cantor's theorem, König's theorem, Konig's theorem

Definition of cardinals

@[implicit_reducible]

instance Cardinal.isEquivalent : Setoid (Type u)

The equivalence relation on types given by equivalence (bijective correspondence) of types. Quotienting by this equivalence relation gives the cardinal numbers.

def Cardinal : Type (u + 1)

Cardinal.{u} is the type of cardinal numbers in Type u, defined as the quotient of Type u by existence of an equivalence (a bijection with explicit inverse).

def Cardinal.mk : Type u → Cardinal.{u}

The cardinal number of a type

def Cardinal.«term#_» : Lean.ParserDescr

The cardinal number of a type

instance Cardinal.canLiftCardinalType : CanLift Cardinal.{u} (Type u) mk fun (x : Cardinal.{u}) => True

theorem Cardinal.inductionOn {motive : Cardinal.{u_1} → Prop} (c : Cardinal.{u_1}) (mk : ∀ (α : Type u_1), motive (mk α)) : motive c

theorem Cardinal.inductionOn₂ {motive : Cardinal.{u_1} → Cardinal.{u_2} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}) (mk : ∀ (α : Type u_1) (β : Type u_2), motive (mk α) (mk β)) : motive c₁ c₂

theorem Cardinal.inductionOn₃ {motive : Cardinal.{u_1} → Cardinal.{u_2} → Cardinal.{u_3} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}) (c₃ : Cardinal.{u_3}) (mk : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), motive (mk α) (mk β) (mk γ)) : motive c₁ c₂ c₃

theorem Cardinal.induction_on_pi {ι : Type u_1} {motive : (ι → Cardinal.{v}) → Prop} (f : ι → Cardinal.{v}) (mk : ∀ (f : ι → Type v), motive fun (i : ι) => mk (f i)) : motive f

theorem Cardinal.eq {α β : Type u} : mk α = mk β ↔ Nonempty (α ≃ β)

@[simp]

theorem Cardinal.mk_out (c : Cardinal.{u_1}) : mk (Quotient.out c) = c

noncomputable def Cardinal.outMkEquiv {α : Type v} : Quotient.out (mk α) ≃ α

The representative of the cardinal of a type is equivalent to the original type.

theorem Cardinal.mk_congr {α β : Type u} (e : α ≃ β) : mk α = mk β

theorem Equiv.cardinal_eq {α β : Type u} (e : α ≃ β) : Cardinal.mk α = Cardinal.mk β

Alias of Cardinal.mk_congr.

def Cardinal.map (f : Type u → Type v) (hf : (α β : Type u) → α ≃ β → f α ≃ f β) : Cardinal.{u} → Cardinal.{v}

Lift a function between Type*s to a function between Cardinals.

@[simp]

theorem Cardinal.map_mk (f : Type u → Type v) (hf : (α β : Type u) → α ≃ β → f α ≃ f β) (α : Type u) : map f hf (mk α) = mk (f α)

def Cardinal.map₂ (f : Type u → Type v → Type w) (hf : (α β : Type u) → (γ δ : Type v) → α ≃ β → γ ≃ δ → f α γ ≃ f β δ) : Cardinal.{u} → Cardinal.{v} → Cardinal.{w}

Lift a binary operation Type* → Type* → Type* to a binary operation on Cardinals.

Lifting cardinals to a higher universe

def Cardinal.lift (c : Cardinal.{v}) : Cardinal.{max v u}

The universe lift operation on cardinals. You can specify the universes explicitly with lift.{u v} : Cardinal.{v} → Cardinal.{max v u}

@[simp]

theorem Cardinal.mk_uLift (α : Type u) : mk (ULift.{v, u} α) = lift.{v, u} (mk α)

theorem Cardinal.lift_umax : lift.{max u v, u} = lift.{v, u}

lift.{max u v, u} equals lift.{v, u}.

Unfortunately, the simp lemma doesn't work.

theorem Cardinal.lift_id' (a : Cardinal.{max u v}) : lift.{u, max u v} a = a

A cardinal lifted to a lower or equal universe equals itself.

Unfortunately, the simp lemma doesn't work.

@[simp]

theorem Cardinal.lift_id (a : Cardinal.{u}) : lift.{u, u} a = a

A cardinal lifted to the same universe equals itself.

@[simp]

theorem Cardinal.lift_uzero (a : Cardinal.{u}) : lift.{0, u} a = a

A cardinal lifted to the zero universe equals itself.

@[simp]

theorem Cardinal.lift_lift (a : Cardinal.{u_1}) : lift.{w, max v u_1} (lift.{v, u_1} a) = lift.{max v w, u_1} a

theorem Cardinal.out_lift_equiv (a : Cardinal.{u}) : Nonempty (Quotient.out (lift.{v, u} a) ≃ Quotient.out a)

theorem Cardinal.lift_mk_eq {α : Type u} {β : Type v} : lift.{max v w, u} (mk α) = lift.{max u w, v} (mk β) ↔ Nonempty (α ≃ β)

theorem Cardinal.lift_mk_eq' {α : Type u} {β : Type v} : lift.{v, u} (mk α) = lift.{u, v} (mk β) ↔ Nonempty (α ≃ β)

A variant of Cardinal.lift_mk_eq with specialized universes. Because Lean often cannot realize it should use this specialization itself, we provide this statement separately so you don't have to solve the specialization problem either.

theorem Cardinal.mk_congr_lift {α : Type u} {β : Type v} (e : α ≃ β) : lift.{v, u} (mk α) = lift.{u, v} (mk β)

theorem Equiv.lift_cardinal_eq {α : Type u} {β : Type v} (e : α ≃ β) : Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β)

Alias of Cardinal.mk_congr_lift.

Basic cardinals

@[implicit_reducible]

instance Cardinal.instZero : Zero Cardinal.{u}

@[implicit_reducible]

instance Cardinal.instInhabited : Inhabited Cardinal.{u}

@[simp]

theorem Cardinal.mk_eq_zero (α : Type u) [IsEmpty α] : mk α = 0

@[simp]

theorem Cardinal.lift_zero : lift.{u_2, u_1} 0 = 0

theorem Cardinal.mk_eq_zero_iff {α : Type u} : mk α = 0 ↔ IsEmpty α

theorem Cardinal.mk_ne_zero_iff {α : Type u} : mk α ≠ 0 ↔ Nonempty α

@[simp]

theorem Cardinal.mk_ne_zero (α : Type u) [Nonempty α] : mk α ≠ 0

theorem Cardinal.nonempty_out {x : Cardinal.{u_1}} (h : x ≠ 0) : Nonempty (Quotient.out x)

@[implicit_reducible]

instance Cardinal.instOne : One Cardinal.{u}

instance Cardinal.instNontrivial : Nontrivial Cardinal.{u}

theorem Cardinal.mk_eq_one (α : Type u) [Subsingleton α] [Nonempty α] : mk α = 1

@[implicit_reducible]

instance Cardinal.instAdd : Add Cardinal.{u}

theorem Cardinal.add_def (α β : Type u) : mk α + mk β = mk (α ⊕ β)

@[implicit_reducible]

instance Cardinal.instNatCast : NatCast Cardinal.{u}

@[simp]

theorem Cardinal.mk_sum (α : Type u) (β : Type v) : mk (α ⊕ β) = lift.{v, u} (mk α) + lift.{u, v} (mk β)

@[simp]

theorem Cardinal.mk_option {α : Type u} : mk (Option α) = mk α + 1

@[simp]

theorem Cardinal.mk_psum (α : Type u) (β : Type v) : mk (α ⊕' β) = lift.{v, u} (mk α) + lift.{u, v} (mk β)

@[implicit_reducible]

instance Cardinal.instMul : Mul Cardinal.{u}

theorem Cardinal.mul_def (α β : Type u) : mk α * mk β = mk (α × β)

@[simp]

theorem Cardinal.mk_prod (α : Type u) (β : Type v) : mk (α × β) = lift.{v, u} (mk α) * lift.{u, v} (mk β)

@[implicit_reducible]

instance Cardinal.instPowCardinal : Pow Cardinal.{u} Cardinal.{u}

The cardinal exponential. #α ^ #β is the cardinal of β → α.

theorem Cardinal.power_def (α β : Type u) : mk α ^ mk β = mk (β → α)

theorem Cardinal.mk_arrow (α : Type u) (β : Type v) : mk (α → β) = lift.{u, v} (mk β) ^ lift.{v, u} (mk α)

@[simp]

theorem Cardinal.lift_power (a b : Cardinal.{u}) : lift.{v, u} (a ^ b) = lift.{v, u} a ^ lift.{v, u} b

@[simp]

theorem Cardinal.power_zero (a : Cardinal.{u_1}) : a ^ 0 = 1

@[simp]

theorem Cardinal.power_one (a : Cardinal.{u}) : a ^ 1 = a

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

@[simp]

theorem Cardinal.one_power {a : Cardinal.{u_1}} : 1 ^ a = 1

@[simp]

theorem Cardinal.zero_power {a : Cardinal.{u_1}} : a ≠ 0 → 0 ^ a = 0

theorem Cardinal.power_ne_zero {a : Cardinal.{u_1}} (b : Cardinal.{u_1}) : a ≠ 0 → a ^ b ≠ 0

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

@[simp]

theorem Cardinal.lift_one : lift.{u_2, u_1} 1 = 1

@[simp]

theorem Cardinal.lift_add (a b : Cardinal.{u}) : lift.{v, u} (a + b) = lift.{v, u} a + lift.{v, u} b

Indexed cardinal sum

def Cardinal.sum {ι : Type u_1} (f : ι → Cardinal.{u_2}) : Cardinal.{max u_2 u_1}

The indexed sum of cardinals is the cardinality of the indexed disjoint union, i.e. sigma type.

@[simp]

theorem Cardinal.mk_sigma {ι : Type u_2} (f : ι → Type u_1) : mk ((i : ι) × f i) = sum fun (i : ι) => mk (f i)

theorem Cardinal.mk_sigma_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι') (h : ∀ (i : ι), lift.{w', w} (mk (f i)) = lift.{w, w'} (mk (g (e i)))) : lift.{max v' w', max w v} (mk ((i : ι) × f i)) = lift.{max v w, max w' v'} (mk ((i : ι') × g i))

theorem Cardinal.mk_sigma_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ (i : ι), mk (f i) = mk (g (e i))) : mk ((i : ι) × f i) = mk ((i : ι') × g i)

theorem Cardinal.mk_sigma_congr' {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)} (e : ι ≃ ι') (h : ∀ (i : ι), mk (f i) = mk (g (e i))) : mk ((i : ι) × f i) = mk ((i : ι') × g i)

Similar to mk_sigma_congr with indexing types in different universes. This is not a strict generalization.

theorem Cardinal.mk_sigma_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ (i : ι), mk (f i) = mk (g i)) : mk ((i : ι) × f i) = mk ((i : ι) × g i)

theorem Cardinal.mk_psigma_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ (i : ι), mk (f i) = mk (g i)) : mk ((i : ι) ×' f i) = mk ((i : ι) ×' g i)

theorem Cardinal.mk_psigma_congrRight_prop {ι : Prop} {f g : ι → Type v} (h : ∀ (i : ι), mk (f i) = mk (g i)) : mk ((i : ι) ×' f i) = mk ((i : ι) ×' g i)

theorem Cardinal.mk_sigma_arrow {ι : Type u_3} (α : Type u_1) (f : ι → Type u_2) : mk (Sigma f → α) = mk ((i : ι) → f i → α)

@[simp]

theorem Cardinal.sum_const (ι : Type u) (a : Cardinal.{v}) : (sum fun (x : ι) => a) = lift.{v, u} (mk ι) * lift.{u, v} a

theorem Cardinal.sum_const' (ι : Type u) (a : Cardinal.{u}) : (sum fun (x : ι) => a) = mk ι * a

@[simp]

theorem Cardinal.lift_sum {ι : Type u} (f : ι → Cardinal.{v}) : lift.{w, max v u} (sum f) = sum fun (i : ι) => lift.{w, v} (f i)

theorem Cardinal.sum_nat_eq_add_sum_succ (f : ℕ → Cardinal.{u}) : sum f = f 0 + sum fun (i : ℕ) => f (i + 1)

Indexed cardinal prod

def Cardinal.prod {ι : Type u} (f : ι → Cardinal.{u_1}) : Cardinal.{max u u_1}

The indexed product of cardinals is the cardinality of the Pi type (dependent product).

@[simp]

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

theorem Cardinal.mk_pi_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι') (h : ∀ (i : ι), lift.{w', w} (mk (f i)) = lift.{w, w'} (mk (g (e i)))) : lift.{max v' w', max v w} (mk ((i : ι) → f i)) = lift.{max v w, max v' w'} (mk ((i : ι') → g i))

theorem Cardinal.mk_pi_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ (i : ι), mk (f i) = mk (g (e i))) : mk ((i : ι) → f i) = mk ((i : ι') → g i)

theorem Cardinal.mk_pi_congr_prop {ι ι' : Prop} {f : ι → Type v} {g : ι' → Type v} (e : ι ↔ ι') (h : ∀ (i : ι), mk (f i) = mk (g ⋯)) : mk ((i : ι) → f i) = mk ((i : ι') → g i)

theorem Cardinal.mk_pi_congr' {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)} (e : ι ≃ ι') (h : ∀ (i : ι), mk (f i) = mk (g (e i))) : mk ((i : ι) → f i) = mk ((i : ι') → g i)

Similar to mk_pi_congr with indexing types in different universes. This is not a strict generalization.

theorem Cardinal.mk_pi_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ (i : ι), mk (f i) = mk (g i)) : mk ((i : ι) → f i) = mk ((i : ι) → g i)

theorem Cardinal.mk_pi_congrRight_prop {ι : Prop} {f g : ι → Type v} (h : ∀ (i : ι), mk (f i) = mk (g i)) : mk ((i : ι) → f i) = mk ((i : ι) → g i)

@[simp]

theorem Cardinal.prod_const (ι : Type u) (a : Cardinal.{v}) : (prod fun (x : ι) => a) = lift.{u, v} a ^ lift.{v, u} (mk ι)

theorem Cardinal.prod_const' (ι : Type u) (a : Cardinal.{u}) : (prod fun (x : ι) => a) = a ^ mk ι

@[simp]

theorem Cardinal.prod_eq_zero {ι : Type u_1} (f : ι → Cardinal.{u}) : prod f = 0 ↔ ∃ (i : ι), f i = 0

theorem Cardinal.prod_ne_zero {ι : Type u_1} (f : ι → Cardinal.{u_2}) : prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

theorem Cardinal.lift_power_sum {ι : Type u} (a : Cardinal.{v}) (f : ι → Cardinal.{v}) : lift.{u, v} a ^ sum f = prod fun (i : ι) => a ^ f i

theorem Cardinal.power_sum {ι : Type u} (a : Cardinal.{max u v}) (f : ι → Cardinal.{max u v}) : a ^ sum f = prod fun (i : ι) => a ^ f i

@[simp]

theorem Cardinal.lift_prod {ι : Type u} (c : ι → Cardinal.{v}) : lift.{w, max v u} (prod c) = prod fun (i : ι) => lift.{w, v} (c i)

The first infinite cardinal aleph0

def Cardinal.aleph0 : Cardinal.{u}

ℵ₀ is the smallest infinite cardinal.

Conventions for notations in identifiers:

• The recommended spelling of ℵ₀ in identifiers is aleph0.

def Cardinal.termℵ₀ : Lean.ParserDescr

ℵ₀ is the smallest infinite cardinal.

Conventions for notations in identifiers:

• The recommended spelling of ℵ₀ in identifiers is aleph0.

theorem Cardinal.mk_nat : mk ℕ = aleph0

theorem Cardinal.aleph0_ne_zero : aleph0 ≠ 0

@[simp]

theorem Cardinal.lift_aleph0 : lift.{u_1, u_2} aleph0 = aleph0

theorem Cardinal.lift_mk_fin (n : ℕ) : lift.{u_1, 0} (mk (Fin n)) = ↑n

Cardinalities of basic sets and types

theorem Cardinal.mk_empty : mk Empty = 0

theorem Cardinal.mk_pempty : mk PEmpty.{u_1 + 1} = 0

theorem Cardinal.mk_punit : mk PUnit.{u_1 + 1} = 1

theorem Cardinal.mk_unit : mk Unit = 1

theorem Cardinal.mk_plift_true : mk (PLift True) = 1

theorem Cardinal.mk_plift_false : mk (PLift False) = 0

theorem Cardinal.mk_subtype_of_equiv {α β : Type u} (p : β → Prop) (e : α ≃ β) : mk { a : α // p (e a) } = mk { b : β // p b }