Cardinal Numbers
We define cardinal numbers as a quotient of types under the equivalence relation of equinumerity. We define the order on cardinal numbers, define omega, and do basic cardinal arithmetic: addition, multiplication, power, cardinal successor, minimum, supremum, infinitary sums and products
The fact that the cardinality of α × α coincides with that of α when α is infinite is not
proved in this file, as it relies on facts on well-orders. Instead, it is in
cardinal_ordinal.lean (together with many other facts on cardinals, for instance the
cardinality of list α).
Implementation notes
- There is a type of cardinal numbers in every universe level:
cardinal.{u} : Type (u + 1)is the quotient of types inType u. There is a lift operation lifting cardinal numbers to a higher level. - Cardinal arithmetic specifically for infinite cardinals (like
κ * κ = κ) is in the fileset_theory/ordinal.lean, because concepts from that file are used in the proof.
References
Tags
cardinal number, cardinal arithmetic, cardinal exponentiation, omega
@[instance]
The equivalence relation on types given by equivalence (bijective correspondence) of types. Quotienting by this equivalence relation gives the cardinal numbers.
The cardinal number of a type
Equations
@[instance]
We define the order on cardinal numbers by mk α ≤ mk β if and only if
there exists an embedding (injective function) from α to β.
Equations
- cardinal.has_le = {le := λ (q₁ q₂ : cardinal), quotient.lift_on₂ q₁ q₂ (λ (α β : Type u), nonempty (α ↪ β)) cardinal.has_le._proof_1}
theorem
cardinal.mk_le_of_injective
{α β : Type u}
{f : α → β} :
function.injective f → cardinal.mk α ≤ cardinal.mk β
theorem
cardinal.mk_le_of_surjective
{α β : Type u}
{f : α → β} :
function.surjective f → cardinal.mk β ≤ cardinal.mk α
theorem
cardinal.le_mk_iff_exists_set
{c : cardinal}
{α : Type u} :
c ≤ cardinal.mk α ↔ ∃ (p : set α), cardinal.mk ↥p = c
theorem
cardinal.out_embedding
{c c' : cardinal} :
c ≤ c' ↔ nonempty (quotient.out c ↪ quotient.out c')
@[instance]
Equations
- cardinal.linear_order = {le := has_le.le cardinal.has_le, lt := partial_order.lt._default has_le.le, le_refl := cardinal.linear_order._proof_1, le_trans := cardinal.linear_order._proof_2, lt_iff_le_not_le := cardinal.linear_order._proof_3, le_antisymm := cardinal.linear_order._proof_4, le_total := cardinal.linear_order._proof_5}
@[instance]
@[instance]
@[instance]
Equations
- cardinal.inhabited = {default := 0}
@[instance]
Equations
- cardinal.has_add = {add := λ (q₁ q₂ : cardinal), quotient.lift_on₂ q₁ q₂ (λ (α β : Type u), cardinal.mk (α ⊕ β)) cardinal.has_add._proof_1}
@[simp]
theorem
cardinal.add_def
(α β : Type (max u_1 u_2)) :
cardinal.mk α + cardinal.mk β = cardinal.mk (α ⊕ β)
@[instance]
Equations
- cardinal.has_mul = {mul := λ (q₁ q₂ : cardinal), quotient.lift_on₂ q₁ q₂ (λ (α β : Type u), cardinal.mk (α × β)) cardinal.has_mul._proof_1}
@[simp]
@[instance]
Equations
- cardinal.comm_semiring = {add := has_add.add cardinal.has_add, add_assoc := cardinal.comm_semiring._proof_1, zero := 0, zero_add := zero_add, add_zero := cardinal.comm_semiring._proof_2, add_comm := add_comm, mul := has_mul.mul cardinal.has_mul, mul_assoc := cardinal.comm_semiring._proof_3, one := 1, one_mul := one_mul, mul_one := cardinal.comm_semiring._proof_4, zero_mul := zero_mul, mul_zero := cardinal.comm_semiring._proof_5, left_distrib := left_distrib, right_distrib := cardinal.comm_semiring._proof_6, mul_comm := mul_comm}
The cardinal exponential. mk α ^ mk β is the cardinal of β → α.
Equations
- a.power b = quotient.lift_on₂ a b (λ (α β : Type u), cardinal.mk (β → α)) cardinal.power._proof_1
@[instance]
Equations
@[simp]
@[instance]
Equations
- cardinal.order_bot = {bot := 0, le := linear_order.le cardinal.linear_order, lt := linear_order.lt cardinal.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := cardinal.zero_le}
@[instance]
Equations
- cardinal.canonically_ordered_add_monoid = {add := comm_semiring.add cardinal.comm_semiring, add_assoc := _, zero := comm_semiring.zero cardinal.comm_semiring, zero_add := _, add_zero := _, add_comm := _, le := order_bot.le cardinal.order_bot, lt := order_bot.lt cardinal.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := cardinal.canonically_ordered_add_monoid._proof_1, lt_of_add_lt_add_left := cardinal.canonically_ordered_add_monoid._proof_2, bot := order_bot.bot cardinal.order_bot, bot_le := _, le_iff_exists_add := cardinal.le_iff_exists_add}
@[instance]
Equations
The minimum cardinal in a family of cardinals (the existence
of which is provided by injective_min).
Equations
- cardinal.min I f = f (classical.some _)
theorem
cardinal.min_eq
{ι : Type u_1}
(I : nonempty ι)
(f : ι → cardinal) :
∃ (i : ι), cardinal.min I f = f i
theorem
cardinal.min_le
{ι : Type u_1}
{I : nonempty ι}
(f : ι → cardinal)
(i : ι) :
cardinal.min I f ≤ f i
theorem
cardinal.le_min
{ι : Type u_1}
{I : nonempty ι}
{f : ι → cardinal}
{a : cardinal} :
a ≤ cardinal.min I f ↔ ∀ (i : ι), a ≤ f i
@[instance]
Equations
- cardinal.has_wf = {r := has_lt.lt (preorder.to_has_lt cardinal), wf := cardinal.wf}
The successor cardinal - the smallest cardinal greater than
c. This is not the same as c + 1 except in the case of finite c.
Equations
- c.succ = cardinal.min _ subtype.val
The indexed sum of cardinals is the cardinality of the indexed disjoint union, i.e. sigma type.
Equations
- cardinal.sum f = cardinal.mk (Σ (i : ι), quotient.out (f i))
@[simp]
theorem
cardinal.sum_mk
{ι : Type u_1}
(f : ι → Type u_2) :
cardinal.sum (λ (i : ι), cardinal.mk (f i)) = cardinal.mk (Σ (i : ι), f i)
theorem
cardinal.sum_const
(ι : Type u)
(a : cardinal) :
cardinal.sum (λ (_x : ι), a) = cardinal.mk ι * a
theorem
cardinal.sum_le_sum
{ι : Type u_1}
(f g : ι → cardinal) :
(∀ (i : ι), f i ≤ g i) → cardinal.sum f ≤ cardinal.sum g
The indexed supremum of cardinals is the smallest cardinal above everything in the family.
Equations
- cardinal.sup f = cardinal.min _ (λ (a : {c // ∀ (i : ι), f i ≤ c}), a.val)
theorem
cardinal.sup_le
{ι : Type u_1}
{f : ι → cardinal}
{a : cardinal} :
cardinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
theorem
cardinal.sup_le_sup
{ι : Type u_1}
(f g : ι → cardinal) :
(∀ (i : ι), f i ≤ g i) → cardinal.sup f ≤ cardinal.sup g
theorem
cardinal.sum_le_sup
{ι : Type u}
(f : ι → cardinal) :
cardinal.sum f ≤ cardinal.mk ι * cardinal.sup f
The indexed product of cardinals is the cardinality of the Pi type (dependent product).
Equations
- cardinal.prod f = cardinal.mk (Π (i : ι), quotient.out (f i))
@[simp]
theorem
cardinal.prod_mk
{ι : Type u_1}
(f : ι → Type u_2) :
cardinal.prod (λ (i : ι), cardinal.mk (f i)) = cardinal.mk (Π (i : ι), f i)
theorem
cardinal.prod_const
(ι : Type u)
(a : cardinal) :
cardinal.prod (λ (_x : ι), a) = a ^ cardinal.mk ι
theorem
cardinal.prod_le_prod
{ι : Type u_1}
(f g : ι → cardinal) :
(∀ (i : ι), f i ≤ g i) → cardinal.prod f ≤ cardinal.prod g
theorem
cardinal.prod_ne_zero
{ι : Type u_1}
(f : ι → cardinal) :
cardinal.prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
theorem
cardinal.prod_eq_zero
{ι : Type u_1}
(f : ι → cardinal) :
cardinal.prod f = 0 ↔ ∃ (i : ι), f i = 0
theorem
cardinal.lift_mk_le
{α : Type u}
{β : Type v} :
(cardinal.mk α).lift ≤ (cardinal.mk β).lift ↔ nonempty (α ↪ β)
theorem
cardinal.lift_mk_eq
{α : Type u}
{β : Type v} :
(cardinal.mk α).lift = (cardinal.mk β).lift ↔ nonempty (α ≃ β)
@[simp]
theorem
cardinal.lift_min
{ι : Type u_1}
{I : nonempty ι}
(f : ι → cardinal) :
(cardinal.min I f).lift = cardinal.min I (cardinal.lift ∘ f)
theorem
cardinal.mk_prod
{α : Type u}
{β : Type v} :
cardinal.mk (α × β) = (cardinal.mk α).lift * (cardinal.mk β).lift
theorem
cardinal.sum_const_eq_lift_mul
(ι : Type u)
(a : cardinal) :
cardinal.sum (λ (_x : ι), a) = (cardinal.mk ι).lift * a.lift
ω is the smallest infinite cardinal, also known as ℵ₀.
Equations
theorem
cardinal.lt_omega_iff_fintype
{α : Type u} :
cardinal.mk α < cardinal.omega ↔ nonempty (fintype α)
@[instance]
Equations
- cardinal.can_lift_cardinal_nat = {coe := coe coe_to_lift, cond := λ (x : cardinal), x < cardinal.omega, prf := cardinal.can_lift_cardinal_nat._proof_1}
theorem
cardinal.add_lt_omega
{a b : cardinal} :
a < cardinal.omega → b < cardinal.omega → a + b < cardinal.omega
theorem
cardinal.add_lt_omega_iff
{a b : cardinal} :
a + b < cardinal.omega ↔ a < cardinal.omega ∧ b < cardinal.omega
theorem
cardinal.mul_lt_omega
{a b : cardinal} :
a < cardinal.omega → b < cardinal.omega → a * b < cardinal.omega
theorem
cardinal.mul_lt_omega_iff
{a b : cardinal} :
a * b < cardinal.omega ↔ a = 0 ∨ b = 0 ∨ a < cardinal.omega ∧ b < cardinal.omega
theorem
cardinal.mul_lt_omega_iff_of_ne_zero
{a b : cardinal} :
a ≠ 0 → b ≠ 0 → (a * b < cardinal.omega ↔ a < cardinal.omega ∧ b < cardinal.omega)
theorem
cardinal.power_lt_omega
{a b : cardinal} :
a < cardinal.omega → b < cardinal.omega → a ^ b < cardinal.omega
theorem
cardinal.eq_one_iff_subsingleton_and_nonempty
{α : Type u_1} :
cardinal.mk α = 1 ↔ subsingleton α ∧ nonempty α
theorem
cardinal.sum_lt_prod
{ι : Type u_1}
(f g : ι → cardinal) :
(∀ (i : ι), f i < g i) → cardinal.sum f < cardinal.prod g
König's theorem
@[simp]
theorem
cardinal.mk_list_eq_sum_pow
(α : Type u) :
cardinal.mk (list α) = cardinal.sum (λ (n : ℕ), cardinal.mk α ^ ↑n)
theorem
cardinal.mk_quotient_le
{α : Type u}
{s : setoid α} :
cardinal.mk (quotient s) ≤ cardinal.mk α
theorem
cardinal.mk_subtype_le
{α : Type u}
(p : α → Prop) :
cardinal.mk (subtype p) ≤ cardinal.mk α
theorem
cardinal.mk_subtype_le_of_subset
{α : Type u}
{p q : α → Prop} :
(∀ ⦃x : α⦄, p x → q x) → cardinal.mk (subtype p) ≤ cardinal.mk (subtype q)
theorem
cardinal.mk_image_le
{α β : Type u}
{f : α → β}
{s : set α} :
cardinal.mk ↥(f '' s) ≤ cardinal.mk ↥s
theorem
cardinal.mk_image_le_lift
{α : Type u}
{β : Type v}
{f : α → β}
{s : set α} :
(cardinal.mk ↥(f '' s)).lift ≤ (cardinal.mk ↥s).lift
theorem
cardinal.mk_range_le
{α β : Type u}
{f : α → β} :
cardinal.mk ↥(set.range f) ≤ cardinal.mk α
theorem
cardinal.mk_range_eq
{α β : Type u}
(f : α → β) :
function.injective f → cardinal.mk ↥(set.range f) = cardinal.mk α
theorem
cardinal.mk_range_eq_of_injective
{α : Type u}
{β : Type v}
{f : α → β} :
function.injective f → (cardinal.mk ↥(set.range f)).lift = (cardinal.mk α).lift
theorem
cardinal.mk_range_eq_lift
{α : Type u}
{β : Type v}
{f : α → β} :
function.injective f → (cardinal.mk ↥(set.range f)).lift = (cardinal.mk α).lift
theorem
cardinal.mk_image_eq
{α β : Type u}
{f : α → β}
{s : set α} :
function.injective f → cardinal.mk ↥(f '' s) = cardinal.mk ↥s
theorem
cardinal.mk_Union_le_sum_mk
{α ι : Type u}
{f : ι → set α} :
cardinal.mk (↥⋃ (i : ι), f i) ≤ cardinal.sum (λ (i : ι), cardinal.mk ↥(f i))
theorem
cardinal.mk_Union_eq_sum_mk
{α ι : Type u}
{f : ι → set α} :
(∀ (i j : ι), i ≠ j → disjoint (f i) (f j)) → cardinal.mk (↥⋃ (i : ι), f i) = cardinal.sum (λ (i : ι), cardinal.mk ↥(f i))
theorem
cardinal.mk_Union_le
{α ι : Type u}
(f : ι → set α) :
cardinal.mk (↥⋃ (i : ι), f i) ≤ cardinal.mk ι * cardinal.sup (λ (i : ι), cardinal.mk ↥(f i))
theorem
cardinal.mk_sUnion_le
{α : Type u}
(A : set (set α)) :
cardinal.mk (↥⋃₀A) ≤ cardinal.mk ↥A * cardinal.sup (λ (s : ↥A), cardinal.mk ↥s)
theorem
cardinal.mk_bUnion_le
{ι α : Type u}
(A : ι → set α)
(s : set ι) :
cardinal.mk (↥⋃ (x : ι) (H : x ∈ s), A x) ≤ cardinal.mk ↥s * cardinal.sup (λ (x : ↥s), cardinal.mk ↥(A x.val))
@[simp]
theorem
cardinal.mk_union_add_mk_inter
{α : Type u}
{S T : set α} :
cardinal.mk ↥(S ∪ T) + cardinal.mk ↥(S ∩ T) = cardinal.mk ↥S + cardinal.mk ↥T
theorem
cardinal.mk_union_le
{α : Type u}
(S T : set α) :
cardinal.mk ↥(S ∪ T) ≤ cardinal.mk ↥S + cardinal.mk ↥T
The cardinality of a union is at most the sum of the cardinalities of the two sets.
theorem
cardinal.mk_union_of_disjoint
{α : Type u}
{S T : set α} :
disjoint S T → cardinal.mk ↥(S ∪ T) = cardinal.mk ↥S + cardinal.mk ↥T
theorem
cardinal.mk_sum_compl
{α : Type u_1}
(s : set α) :
cardinal.mk ↥s + cardinal.mk ↥sᶜ = cardinal.mk α
theorem
cardinal.mk_le_mk_of_subset
{α : Type u_1}
{s t : set α} :
s ⊆ t → cardinal.mk ↥s ≤ cardinal.mk ↥t
theorem
cardinal.mk_subtype_mono
{α : Type u}
{p q : α → Prop} :
(∀ (x : α), p x → q x) → cardinal.mk {x // p x} ≤ cardinal.mk {x // q x}
theorem
cardinal.mk_image_eq_lift
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
function.injective f → (cardinal.mk ↥(f '' s)).lift = (cardinal.mk ↥s).lift
theorem
cardinal.mk_image_eq_of_inj_on_lift
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.inj_on f s → (cardinal.mk ↥(f '' s)).lift = (cardinal.mk ↥s).lift
theorem
cardinal.mk_image_eq_of_inj_on
{α β : Type u}
(f : α → β)
(s : set α) :
set.inj_on f s → cardinal.mk ↥(f '' s) = cardinal.mk ↥s
theorem
cardinal.mk_subtype_of_equiv
{α β : Type u}
(p : β → Prop)
(e : α ≃ β) :
cardinal.mk {a // p (⇑e a)} = cardinal.mk {b // p b}
theorem
cardinal.mk_sep
{α : Type u}
(s : set α)
(t : α → Prop) :
cardinal.mk ↥{x ∈ s | t x} = cardinal.mk ↥{x : ↥s | t x.val}
theorem
cardinal.mk_preimage_of_injective_lift
{α : Type u}
{β : Type v}
(f : α → β)
(s : set β) :
function.injective f → (cardinal.mk ↥(f ⁻¹' s)).lift ≤ (cardinal.mk ↥s).lift
theorem
cardinal.mk_preimage_of_subset_range_lift
{α : Type u}
{β : Type v}
(f : α → β)
(s : set β) :
s ⊆ set.range f → (cardinal.mk ↥s).lift ≤ (cardinal.mk ↥(f ⁻¹' s)).lift
theorem
cardinal.mk_preimage_of_injective_of_subset_range_lift
{α : Type u}
{β : Type v}
(f : α → β)
(s : set β) :
function.injective f → s ⊆ set.range f → (cardinal.mk ↥(f ⁻¹' s)).lift = (cardinal.mk ↥s).lift
theorem
cardinal.mk_preimage_of_injective
{α β : Type u}
(f : α → β)
(s : set β) :
function.injective f → cardinal.mk ↥(f ⁻¹' s) ≤ cardinal.mk ↥s
theorem
cardinal.mk_preimage_of_subset_range
{α β : Type u}
(f : α → β)
(s : set β) :
s ⊆ set.range f → cardinal.mk ↥s ≤ cardinal.mk ↥(f ⁻¹' s)
theorem
cardinal.mk_preimage_of_injective_of_subset_range
{α β : Type u}
(f : α → β)
(s : set β) :
function.injective f → s ⊆ set.range f → cardinal.mk ↥(f ⁻¹' s) = cardinal.mk ↥s
theorem
cardinal.mk_subset_ge_of_subset_image_lift
{α : Type u}
{β : Type v}
(f : α → β)
{s : set α}
{t : set β} :
t ⊆ f '' s → (cardinal.mk ↥t).lift ≤ (cardinal.mk ↥{x ∈ s | f x ∈ t}).lift
theorem
cardinal.mk_subset_ge_of_subset_image
{α β : Type u}
(f : α → β)
{s : set α}
{t : set β} :
t ⊆ f '' s → cardinal.mk ↥t ≤ cardinal.mk ↥{x ∈ s | f x ∈ t}
theorem
cardinal.le_mk_iff_exists_subset
{c : cardinal}
{α : Type u}
{s : set α} :
c ≤ cardinal.mk ↥s ↔ ∃ (p : set α), p ⊆ s ∧ cardinal.mk ↥p = c
The function α^{<β}, defined to be sup_{γ < β} α^γ. We index over {s : set β.out // mk s < β } instead of {γ // γ < β}, because the latter lives in a higher universe
Equations
- α ^< β = cardinal.sup (λ (s : {s // cardinal.mk ↥s < β}), α ^ cardinal.mk ↥s)
theorem
cardinal.powerlt_aux
{c c' : cardinal} :
c < c' → (∃ (s : {s // cardinal.mk ↥s < c'}), cardinal.mk ↥s = c)