mathlib documentation

set_theory.cardinal

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

References

Tags

cardinal number, cardinal arithmetic, cardinal exponentiation, omega

@[instance]
def cardinal.is_equivalent  :
setoid (Type u)

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

Equations
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).

Equations
def cardinal.mk  :
Type ucardinal

The cardinal number of a type

Equations
theorem cardinal.eq {α β : Type u} :
# α = # β nonempty β)

@[simp]
theorem cardinal.mk_def (α : Type u) :
α = # α

@[simp]
theorem cardinal.mk_out (c : cardinal) :

@[instance]

We define the order on cardinal numbers by mk α ≤ mk β if and only if there exists an embedding (injective function) from α to β.

Equations
theorem cardinal.mk_le_of_injective {α β : Type u} {f : α → β} :

theorem cardinal.mk_le_of_surjective {α β : Type u} {f : α → β} :

theorem cardinal.le_mk_iff_exists_set {c : cardinal} {α : Type u} :
c # α ∃ (p : set α), # p = c

@[instance]

Equations
theorem cardinal.ne_zero_iff_nonempty {α : Type u} :
# α 0 nonempty α

theorem cardinal.le_one_iff_subsingleton {α : Type u} :

theorem cardinal.one_lt_iff_nontrivial {α : Type u} :
1 < # α nontrivial α

@[instance]

Equations
@[simp]
theorem cardinal.add_def (α β : Type (max u_1 u_2)) :
# α + # β = # β)

@[instance]

Equations
@[simp]
theorem cardinal.mul_def (α β : Type u) :
(# α) * # β = # × β)

@[instance]

Equations

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

Equations
@[simp]
theorem cardinal.power_def (α β : Type u_1) :
# α ^ # β = # (β → α)

@[simp]
theorem cardinal.power_zero {a : cardinal} :
a ^ 0 = 1

@[simp]
theorem cardinal.power_one {a : cardinal} :
a ^ 1 = a

@[simp]
theorem cardinal.one_power {a : cardinal} :
1 ^ a = 1

@[simp]
theorem cardinal.prop_eq_two  :
# (ulift Prop) = 2

@[simp]
theorem cardinal.zero_power {a : cardinal} :
a 00 ^ a = 0

theorem cardinal.power_ne_zero {a : cardinal} (b : cardinal) :
a 0a ^ b 0

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

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

theorem cardinal.power_mul {a b c : cardinal} :
(a ^ b) ^ c = a ^ b * c

@[simp]
theorem cardinal.pow_cast_right (κ : cardinal) (n : ) :
κ ^ n = κ ^ n

theorem cardinal.zero_le (a : cardinal) :
0 a

theorem cardinal.le_zero (a : cardinal) :
a 0 a = 0

theorem cardinal.pos_iff_ne_zero {o : cardinal} :
0 < o o 0

@[simp]
theorem cardinal.zero_lt_one  :
0 < 1

theorem cardinal.zero_power_le (c : cardinal) :
0 ^ c 1

theorem cardinal.add_le_add {a b c d : cardinal} :
a bc da + c b + d

theorem cardinal.add_le_add_left (a : cardinal) {b c : cardinal} :
b ca + b a + c

theorem cardinal.add_le_add_right {a b : cardinal} (c : cardinal) :
a ba + c b + c

theorem cardinal.le_add_right (a b : cardinal) :
a a + b

theorem cardinal.le_add_left (a b : cardinal) :
a b + a

theorem cardinal.mul_le_mul {a b c d : cardinal} :
a bc da * c b * d

theorem cardinal.mul_le_mul_left (a : cardinal) {b c : cardinal} :
b ca * b a * c

theorem cardinal.mul_le_mul_right {a b : cardinal} (c : cardinal) :
a ba * c b * c

theorem cardinal.power_le_power_left {a b c : cardinal} :
a 0b ca ^ b a ^ c

theorem cardinal.power_le_max_power_one {a b c : cardinal} :
b ca ^ b max (a ^ c) 1

theorem cardinal.power_le_power_right {a b c : cardinal} :
a ba ^ c b ^ c

theorem cardinal.le_iff_exists_add {a b : cardinal} :
a b ∃ (c : cardinal), b = a + c

theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a

def cardinal.min {ι : Type u_1} :
nonempty ι(ι → cardinal)cardinal

The minimum cardinal in a family of cardinals (the existence of which is provided by injective_min).

Equations
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 : ι) :

theorem cardinal.le_min {ι : Type u_1} {I : nonempty ι} {f : ι → cardinal} {a : cardinal} :
a cardinal.min I f ∀ (i : ι), a f i

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
theorem cardinal.lt_succ_self (c : cardinal) :
c < c.succ

theorem cardinal.succ_le {a b : cardinal} :
a.succ b a < b

theorem cardinal.lt_succ {a b : cardinal} :
a < b.succ a b

def cardinal.sum {ι : Type u_1} :
(ι → cardinal)cardinal

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

Equations
theorem cardinal.le_sum {ι : Type u_1} (f : ι → cardinal) (i : ι) :

@[simp]
theorem cardinal.sum_mk {ι : Type u_1} (f : ι → Type u_2) :
cardinal.sum (λ (i : ι), # (f i)) = # (Σ (i : ι), f i)

theorem cardinal.sum_const (ι : Type u) (a : cardinal) :
cardinal.sum (λ (_x : ι), a) = (# ι) * a

theorem cardinal.sum_le_sum {ι : Type u_1} (f g : ι → cardinal) :
(∀ (i : ι), f i g i)cardinal.sum f cardinal.sum g

def cardinal.sup {ι : Type u_1} :
(ι → cardinal)cardinal

The indexed supremum of cardinals is the smallest cardinal above everything in the family.

Equations
theorem cardinal.le_sup {ι : Type u_1} (f : ι → cardinal) (i : ι) :

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.sup_le_sum {ι : Type u_1} (f : ι → cardinal) :

theorem cardinal.sum_le_sup {ι : Type u} (f : ι → cardinal) :

theorem cardinal.sup_eq_zero {ι : Type u_1} {f : ι → cardinal} :
(ι → false)cardinal.sup f = 0

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

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

Equations
@[simp]
theorem cardinal.prod_mk {ι : Type u_1} (f : ι → Type u_2) :
cardinal.prod (λ (i : ι), # (f i)) = # (Π (i : ι), f i)

theorem cardinal.prod_const (ι : Type u) (a : cardinal) :
cardinal.prod (λ (_x : ι), a) = a ^ # ι

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

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

Equations
theorem cardinal.lift_mk (α : Type u) :
(# α).lift = # (ulift α)

theorem cardinal.lift_id' (a : cardinal) :
a.lift = a

@[simp]
theorem cardinal.lift_id (a : cardinal) :
a.lift = a

@[simp]
theorem cardinal.lift_lift (a : cardinal) :

theorem cardinal.lift_mk_le {α : Type u} {β : Type v} :
(# α).lift (# β).lift nonempty β)

theorem cardinal.lift_mk_eq {α : Type u} {β : Type v} :
(# α).lift = (# β).lift nonempty β)

@[simp]
theorem cardinal.lift_le {a b : cardinal} :
a.lift b.lift a b

@[simp]
theorem cardinal.lift_inj {a b : cardinal} :
a.lift = b.lift a = b

@[simp]
theorem cardinal.lift_lt {a b : cardinal} :
a.lift < b.lift a < b

@[simp]
theorem cardinal.lift_zero  :
0.lift = 0

@[simp]
theorem cardinal.lift_one  :
1.lift = 1

@[simp]
theorem cardinal.lift_add (a b : cardinal) :
(a + b).lift = a.lift + b.lift

@[simp]
theorem cardinal.lift_mul (a b : cardinal) :
(a * b).lift = (a.lift) * b.lift

@[simp]
theorem cardinal.lift_power (a b : cardinal) :
(a ^ b).lift = a.lift ^ b.lift

@[simp]
theorem cardinal.lift_two_power (a : cardinal) :
(2 ^ a).lift = 2 ^ a.lift

@[simp]
theorem cardinal.lift_min {ι : Type u_1} {I : nonempty ι} (f : ι → cardinal) :

theorem cardinal.lift_down {a : cardinal} {b : cardinal} :
b a.lift(∃ (a' : cardinal), a'.lift = b)

theorem cardinal.le_lift_iff {a : cardinal} {b : cardinal} :
b a.lift ∃ (a' : cardinal), a'.lift = b a' a

theorem cardinal.lt_lift_iff {a : cardinal} {b : cardinal} :
b < a.lift ∃ (a' : cardinal), a'.lift = b a' < a

@[simp]
theorem cardinal.lift_succ (a : cardinal) :

@[simp]
theorem cardinal.lift_max {a : cardinal} {b : cardinal} :
a.lift = b.lift a.lift = b.lift

theorem cardinal.mk_prod {α : Type u} {β : Type v} :
# × β) = ((# α).lift) * (# β).lift

theorem cardinal.sum_const_eq_lift_mul (ι : Type u) (a : cardinal) :
cardinal.sum (λ (_x : ι), a) = ((# ι).lift) * a.lift

ω is the smallest infinite cardinal, also known as ℵ₀.

Equations
@[simp]
theorem cardinal.mk_fin (n : ) :
# (fin n) = n

@[simp]
theorem cardinal.lift_nat_cast (n : ) :

theorem cardinal.lift_eq_nat_iff {a : cardinal} {n : } :
a.lift = n a = n

theorem cardinal.nat_eq_lift_eq_iff {n : } {a : cardinal} :
n = a.lift n = a

theorem cardinal.lift_mk_fin (n : ) :
(# (fin n)).lift = n

theorem cardinal.fintype_card (α : Type u) [fintype α] :

theorem cardinal.card_le_of_finset {α : Type u_1} (s : finset α) :
(s.card) # α

@[simp]
theorem cardinal.nat_cast_pow {m n : } :
(m ^ n) = m ^ n

@[simp]
theorem cardinal.nat_cast_le {m n : } :
m n m n

@[simp]
theorem cardinal.nat_cast_lt {m n : } :
m < n m < n

@[simp]
theorem cardinal.nat_cast_inj {m n : } :
m = n m = n

@[simp]
theorem cardinal.nat_succ (n : ) :

@[simp]
theorem cardinal.succ_zero  :
0.succ = 1

theorem cardinal.card_le_of {α : Type u} {n : } :
(∀ (s : finset α), s.card n)# α n

theorem cardinal.cantor' (a : cardinal) {b : cardinal} :
1 < ba < b ^ a

theorem cardinal.one_le_iff_pos {c : cardinal} :
1 c 0 < c

theorem cardinal.lt_omega {c : cardinal} :
c < cardinal.omega ∃ (n : ), c = n

theorem cardinal.omega_le {c : cardinal} :
cardinal.omega c ∀ (n : ), n c

theorem cardinal.lt_omega_iff_finite {α : Type u_1} {S : set α} :

@[instance]

Equations
theorem cardinal.infinite_iff {α : Type u} :

theorem cardinal.countable_iff {α : Type u} (s : set α) :

theorem cardinal.two_le_iff {α : Type u} :
2 # α ∃ (x y : α), x y

theorem cardinal.two_le_iff' {α : Type u} (x : α) :
2 # α ∃ (y : α), x y

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_empty  :

@[simp]
theorem cardinal.mk_pempty  :

@[simp]
theorem cardinal.mk_plift_of_false {p : Prop} :
¬p → # (plift p) = 0

theorem cardinal.mk_unit  :
# unit = 1

@[simp]
theorem cardinal.mk_punit  :

@[simp]
theorem cardinal.mk_singleton {α : Type u} (x : α) :
# {x} = 1

@[simp]
theorem cardinal.mk_plift_of_true {p : Prop} :
p → # (plift p) = 1

@[simp]
theorem cardinal.mk_bool  :
# bool = 2

@[simp]
theorem cardinal.mk_Prop  :
# Prop = 2

@[simp]
theorem cardinal.mk_set {α : Type u} :
# (set α) = 2 ^ # α

@[simp]
theorem cardinal.mk_option {α : Type u} :
# (option α) = # α + 1

theorem cardinal.mk_list_eq_sum_pow (α : Type u) :
# (list α) = cardinal.sum (λ (n : ), # α ^ n)

theorem cardinal.mk_quot_le {α : Type u} {r : α → α → Prop} :
# (quot r) # α

theorem cardinal.mk_quotient_le {α : Type u} {s : setoid α} :
# (quotient s) # α

theorem cardinal.mk_subtype_le {α : Type u} (p : α → Prop) :
# (subtype p) # α

theorem cardinal.mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} :
(∀ ⦃x : α⦄, p xq x)# (subtype p) # (subtype q)

@[simp]
theorem cardinal.mk_emptyc (α : Type u) :

theorem cardinal.mk_emptyc_iff {α : Type u} {s : set α} :
# s = 0 s =

theorem cardinal.mk_univ {α : Type u} :

theorem cardinal.mk_image_le {α β : Type u} {f : α → β} {s : set α} :
# (f '' s) # s

theorem cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(# (f '' s)).lift (# s).lift

theorem cardinal.mk_range_le {α β : Type u} {f : α → β} :

theorem cardinal.mk_range_eq {α β : Type u} (f : α → β) :

theorem cardinal.mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} :

theorem cardinal.mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} :

theorem cardinal.mk_image_eq {α β : Type u} {f : α → β} {s : set α} :

theorem cardinal.mk_Union_le_sum_mk {α ι : Type u} {f : ι → set α} :
# (⋃ (i : ι), f i) cardinal.sum (λ (i : ι), # (f i))

theorem cardinal.mk_Union_eq_sum_mk {α ι : Type u} {f : ι → set α} :
(∀ (i j : ι), i jdisjoint (f i) (f j))# (⋃ (i : ι), f i) = cardinal.sum (λ (i : ι), # (f i))

theorem cardinal.mk_Union_le {α ι : Type u} (f : ι → set α) :
# (⋃ (i : ι), f i) (# ι) * cardinal.sup (λ (i : ι), # (f i))

theorem cardinal.mk_sUnion_le {α : Type u} (A : set (set α)) :
# (⋃₀A) (# A) * cardinal.sup (λ (s : A), # s)

theorem cardinal.mk_bUnion_le {ι α : Type u} (A : ι → set α) (s : set ι) :
# (⋃ (x : ι) (H : x s), A x) (# s) * cardinal.sup (λ (x : s), # (A x.val))

@[simp]
theorem cardinal.finset_card {α : Type u} {s : finset α} :

theorem cardinal.finset_card_lt_omega {α : Type u} (s : finset α) :

theorem cardinal.mk_union_add_mk_inter {α : Type u} {S T : set α} :
# (S T) + # (S T) = # S + # T

theorem cardinal.mk_union_le {α : Type u} (S T : set α) :
# (S T) # S + # 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# (S T) = # S + # T

theorem cardinal.mk_sum_compl {α : Type u_1} (s : set α) :
# s + # s = # α

theorem cardinal.mk_le_mk_of_subset {α : Type u_1} {s t : set α} :
s t# s # t

theorem cardinal.mk_subtype_mono {α : Type u} {p q : α → Prop} :
(∀ (x : α), p xq x)# {x // p x} # {x // q x}

theorem cardinal.mk_set_le {α : Type u} (s : set α) :
# s # α

theorem cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : α → β) (s : set α) :

theorem cardinal.mk_image_eq_of_inj_on_lift {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.inj_on f s(# (f '' s)).lift = (# s).lift

theorem cardinal.mk_image_eq_of_inj_on {α β : Type u} (f : α → β) (s : set α) :
set.inj_on f s# (f '' s) = # s

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

theorem cardinal.mk_sep {α : Type u} (s : set α) (t : α → Prop) :
# {x ∈ s | t x} = # {x : s | t x.val}

theorem cardinal.mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : set β) :

theorem cardinal.mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : set β) :
s set.range f(# s).lift (# (f ⁻¹' s)).lift

theorem cardinal.mk_preimage_of_injective_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : set β) :

theorem cardinal.mk_preimage_of_injective {α β : Type u} (f : α → β) (s : set β) :

theorem cardinal.mk_preimage_of_subset_range {α β : Type u} (f : α → β) (s : set β) :
s set.range f# s # (f ⁻¹' s)

theorem cardinal.mk_preimage_of_injective_of_subset_range {α β : Type u} (f : α → β) (s : set β) :

theorem cardinal.mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : set α} {t : set β} :
t f '' s(# t).lift (# {x ∈ s | f x t}).lift

theorem cardinal.mk_subset_ge_of_subset_image {α β : Type u} (f : α → β) {s : set α} {t : set β} :
t f '' s# t # {x ∈ s | f x t}

theorem cardinal.le_mk_iff_exists_subset {c : cardinal} {α : Type u} {s : set α} :
c # s ∃ (p : set α), p s # 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
theorem cardinal.powerlt_aux {c c' : cardinal} :
c < c'(∃ (s : {s // # s < c'}), # s = c)

theorem cardinal.le_powerlt {c₁ c₂ c₃ : cardinal} :
c₂ < c₃c₁ ^ c₂ c₁ ^< c₃

theorem cardinal.powerlt_le {c₁ c₂ c₃ : cardinal} :
c₁ ^< c₂ c₃ ∀ (c₄ : cardinal), c₄ < c₂c₁ ^ c₄ c₃

theorem cardinal.powerlt_le_powerlt_left {a b c : cardinal} :
b ca ^< b a ^< c

theorem cardinal.powerlt_succ {c₁ c₂ : cardinal} :
c₁ 0c₁ ^< c₂.succ = c₁ ^ c₂

theorem cardinal.powerlt_max {c₁ c₂ c₃ : cardinal} :
c₁ ^< max c₂ c₃ = max (c₁ ^< c₂) (c₁ ^< c₃)

theorem cardinal.zero_powerlt {a : cardinal} :
a 00 ^< a = 1

theorem cardinal.powerlt_zero {a : cardinal} :
a ^< 0 = 0