mathlib documentation

set_theory.cardinal

Cardinal Numbers #

We define cardinal numbers as a quotient of types under the equivalence relation of equinumerity.

Main definitions #

Main Statements #

Implementation notes #

References #

Tags #

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

@[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
@[instance]
Equations
theorem cardinal.induction_on {p : cardinal → Prop} (c : cardinal) (h : ∀ (α : Type u_1), p (# α)) :
p c
theorem cardinal.induction_on₂ {p : cardinalcardinal → Prop} (c₁ : cardinal) (c₂ : cardinal) (h : ∀ (α : Type u_1) (β : Type u_2), p (# α) (# β)) :
p c₁ c₂
theorem cardinal.induction_on₃ {p : cardinalcardinalcardinal → Prop} (c₁ : cardinal) (c₂ : cardinal) (c₃ : cardinal) (h : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), p (# α) (# β) (# γ)) :
p c₁ c₂ c₃
theorem cardinal.eq {α β : Type u} :
# α = # β nonempty β)
@[simp]
theorem cardinal.mk_def (α : Type u) :
α = # α
@[simp]
theorem cardinal.mk_out (c : cardinal) :
def cardinal.out_mk_equiv {α : Type v} :

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

Equations
theorem cardinal.mk_congr {α β : Type u} (e : α β) :
# α = # β
theorem equiv.cardinal_eq {α β : Type u} (e : α β) :
# α = # β

Alias of mk_congr.

def cardinal.map (f : Type uType v) (hf : Π (α β : Type u), α βf α f β) :

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

Equations
@[simp]
theorem cardinal.map_mk (f : Type uType v) (hf : Π (α β : Type u), α βf α f β) (α : Type u) :
cardinal.map f hf (# α) = # (f α)
def cardinal.map₂ (f : Type uType vType w) (hf : Π (α β : Type u) (γ δ : Type v), α βγ δf α γ f β δ) :

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

Equations

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

Equations
@[simp]
theorem cardinal.mk_ulift (α : Type u) :
# (ulift α) = (# α).lift
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) :
@[instance]

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

Equations
theorem cardinal.le_def (α β : Type u) :
# α # β nonempty β)
theorem cardinal.mk_le_of_injective {α β : Type u} {f : α → β} (hf : function.injective f) :
# α # β
theorem function.embedding.cardinal_le {α β : Type u} (f : α β) :
# α # β
theorem cardinal.mk_le_of_surjective {α β : Type u} {f : α → β} (hf : function.surjective f) :
# β # α
theorem cardinal.le_mk_iff_exists_set {c : cardinal} {α : Type u} :
c # α ∃ (p : set α), # p = c
@[instance]
Equations
theorem cardinal.lift_mk_le {α : Type u} {β : Type v} :
(# α).lift (# β).lift nonempty β)
theorem cardinal.lift_mk_le' {α : Type u} {β : Type v} :
(# α).lift (# β).lift nonempty β)

A variant of lift_mk_le with specialized universes. Because Lean often can not 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.lift_mk_eq {α : Type u} {β : Type v} :
(# α).lift = (# β).lift nonempty β)
theorem cardinal.lift_mk_eq' {α : Type u} {β : Type v} :
(# α).lift = (# β).lift nonempty β)

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

@[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.mk_eq_zero (α : Type u) [is_empty α] :
# α = 0
@[simp]
theorem cardinal.lift_zero  :
0.lift = 0
theorem cardinal.mk_eq_zero_iff {α : Type u} :
# α = 0 is_empty α
theorem cardinal.mk_ne_zero_iff {α : Type u} :
# α 0 nonempty α
@[simp]
theorem cardinal.mk_ne_zero (α : Type u) [nonempty α] :
# α 0
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 u) :
# α + # β = # β)
theorem cardinal.add (α : Type u) (β : Type v) :
# β) = (# α).lift + (# β).lift
@[simp]
theorem cardinal.mk_option {α : Type u} :
# (option α) = # α + 1
@[instance]
Equations
@[simp]
theorem cardinal.mul_def (α β : Type u) :
(# α) * # β = # × β)
theorem cardinal.mul (α : Type u) (β : Type v) :
# × β) = ((# α).lift) * (# β).lift
theorem cardinal.add_comm (a b : cardinal) :
a + b = b + a
theorem cardinal.mul_comm (a b : cardinal) :
a * b = b * a
theorem cardinal.zero_add (a : cardinal) :
0 + a = a
theorem cardinal.zero_mul (a : cardinal) :
0 * a = 0
theorem cardinal.one_mul (a : cardinal) :
1 * a = a
theorem cardinal.left_distrib (a b c : cardinal) :
a * (b + c) = a * b + a * c
theorem cardinal.eq_zero_or_eq_zero_of_mul_eq_zero {a b : cardinal} :
a * b = 0a = 0 b = 0

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

Equations
@[simp]
theorem cardinal.power_def (α β : Type u_1) :
# α ^ # β = # (β → α)
@[simp]
theorem cardinal.lift_power (a b : cardinal) :
(a ^ b).lift = a.lift ^ b.lift
@[simp]
theorem cardinal.power_zero {a : cardinal} :
a ^ 0 = 1
@[simp]
theorem cardinal.power_one {a : cardinal} :
a ^ 1 = a
theorem cardinal.power_add {a b c : cardinal} :
a ^ (b + c) = (a ^ b) * a ^ c
@[instance]
Equations
@[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_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.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.le_iff_exists_add {a b : cardinal} :
a b ∃ (c : cardinal), b = a + c
@[instance]
Equations
@[simp]
theorem cardinal.zero_lt_one  :
0 < 1
@[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_bit0 (a : cardinal) :
@[simp]
theorem cardinal.lift_bit1 (a : cardinal) :
theorem cardinal.lift_two  :
2.lift = 2
theorem cardinal.lift_two_power (a : cardinal) :
(2 ^ a).lift = 2 ^ a.lift
theorem cardinal.zero_power_le (c : cardinal) :
0 ^ c 1
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} (h : b c) :
a ^ b max (a ^ c) 1
theorem cardinal.power_le_power_right {a b c : cardinal} :
a ba ^ c b ^ c
theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a

Cantor's theorem

def cardinal.min {ι : Type u_1} (I : nonempty ι) (f : ι → 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
@[simp]
theorem cardinal.lt_succ {a b : cardinal} :
a < b.succ a b
theorem cardinal.succ_pos (c : cardinal) :
0 < c.succ
def cardinal.sum {ι : Type u_1} (f : ι → 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) (H : ∀ (i : ι), f i g i) :
def cardinal.sup {ι : Type u_1} (f : ι → 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) (H : ∀ (i : ι), f i g i) :
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} [is_empty ι] :
def cardinal.prod {ι : Type u} (f : ι → 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) (H : ∀ (i : ι), f i g i) :
theorem cardinal.prod_eq_zero {ι : Type u_1} (f : ι → cardinal) :
cardinal.prod f = 0 ∃ (i : ι), f i = 0
theorem cardinal.prod_ne_zero {ι : Type u_1} (f : ι → cardinal) :
cardinal.prod f 0 ∀ (i : ι), f i 0
@[simp]
theorem cardinal.lift_prod {ι : Type u} (c : ι → cardinal) :
(cardinal.prod c).lift = cardinal.prod (λ (i : ι), (c i).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
theorem cardinal.le_sup_iff {ι : Type v} {f : ι → cardinal} {c : cardinal} :
c cardinal.sup f ∀ (b : cardinal), (∀ (i : ι), f i b)c b
theorem cardinal.lift_sup {ι : Type v} (f : ι → cardinal) :
(cardinal.sup f).lift = cardinal.sup (λ (i : ι), (f i).lift)

The lift of a supremum is the supremum of the lifts.

theorem cardinal.lift_sup_le {ι : Type v} (f : ι → cardinal) (t : cardinal) (w : ∀ (i : ι), (f i).lift t) :

To prove that the lift of a supremum is bounded by some cardinal t, it suffices to show that the lift of each cardinal is bounded by t.

@[simp]
theorem cardinal.lift_sup_le_iff {ι : Type v} (f : ι → cardinal) (t : cardinal) :
(cardinal.sup f).lift t ∀ (i : ι), (f i).lift t
theorem cardinal.lift_sup_le_lift_sup {ι : Type v} {ι' : Type v'} (f : ι → cardinal) (f' : ι' → cardinal) (g : ι → ι') (h : ∀ (i : ι), (f i).lift (f' (g i)).lift) :

To prove an inequality between the lifts to a common universe of two different supremums, it suffices to show that the lift of each cardinal from the smaller supremum if bounded by the lift of some cardinal from the larger supremum.

theorem cardinal.lift_sup_le_lift_sup' {ι : Type v} {ι' : Type v'} (f : ι → cardinal) (f' : ι' → cardinal) (g : ι → ι') (h : ∀ (i : ι), (f i).lift (f' (g i)).lift) :

A variant of lift_sup_le_lift_sup with universes specialized via w = v and w' = v'. This is sometimes necessary to avoid universe unification issues.

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

Equations
theorem cardinal.mk_nat  :
theorem cardinal.omega_pos  :
0 < ω
@[simp]
@[simp]
@[simp]
@[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
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 : } (H : ∀ (s : finset α), s.card n) :
# α n
theorem cardinal.cantor' (a : cardinal) {b : cardinal} (hb : 1 < b) :
a < b ^ a
theorem cardinal.one_le_iff_pos {c : cardinal} :
1 c 0 < c
theorem cardinal.nat_lt_omega (n : ) :
@[simp]
theorem cardinal.one_lt_omega  :
1 < ω
theorem cardinal.lt_omega {c : cardinal} :
c < ω ∃ (n : ), c = n
theorem cardinal.omega_le {c : cardinal} :
ω c ∀ (n : ), n c
theorem cardinal.lt_omega_iff_fintype {α : Type u} :
theorem cardinal.lt_omega_iff_finite {α : Type u_1} {S : set α} :
@[instance]
Equations
theorem cardinal.add_lt_omega {a b : cardinal} (ha : a < ω) (hb : b < ω) :
a + b < ω
theorem cardinal.add_lt_omega_iff {a b : cardinal} :
a + b < ω a < ω b < ω
theorem cardinal.mul_lt_omega {a b : cardinal} (ha : a < ω) (hb : b < ω) :
a * b < ω
theorem cardinal.mul_lt_omega_iff {a b : cardinal} :
a * b < ω a = 0 b = 0 a < ω b < ω
theorem cardinal.mul_lt_omega_iff_of_ne_zero {a b : cardinal} (ha : a 0) (hb : b 0) :
a * b < ω a < ω b < ω
theorem cardinal.power_lt_omega {a b : cardinal} (ha : a < ω) (hb : b < ω) :
a ^ b < ω
theorem cardinal.eq_one_iff_unique {α : Type u_1} :
theorem cardinal.infinite_iff {α : Type u} :
theorem cardinal.omega_le_mk (α : Type u) [infinite α] :
ω # α
theorem cardinal.encodable_iff {α : Type u} :
@[simp]
theorem cardinal.mk_le_omega {α : Type u} [encodable α] :
# α ω
theorem cardinal.denumerable_iff {α : Type u} :
@[simp]
theorem cardinal.mk_denumerable (α : Type u) [denumerable α] :
# α = ω
@[simp]
theorem cardinal.mk_set_le_omega {α : Type u} (s : set α) :
@[simp]
@[simp]
@[simp]
theorem cardinal.add_le_omega {c₁ c₂ : cardinal} :
c₁ + c₂ ω c₁ ω c₂ ω

This function sends finite cardinals to the corresponding natural, and infinite cardinals to 0.

Equations
@[simp]
@[simp]
theorem cardinal.mk_to_nat_of_infinite {α : Type u} [h : infinite α] :
@[simp]
theorem cardinal.mk_to_nat_eq_card {α : Type u} [fintype α] :
@[simp]
theorem cardinal.to_nat_congr {α : Type u} {β : Type v} (e : α β) :

This function sends finite cardinals to the corresponding natural, and infinite cardinals to .

Equations
@[simp]
theorem cardinal.mk_to_enat_of_infinite {α : Type u} [h : infinite α] :
@[simp]
theorem cardinal.mk_int  :
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) (H : ∀ (i : ι), f i < g i) :

König's theorem

@[simp]
theorem cardinal.mk_empty  :
@[simp]
theorem cardinal.mk_pempty  :
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} (h : p) :
# (plift p) = 1
@[simp]
theorem cardinal.mk_plift_of_false {p : Prop} (h : ¬p) :
# (plift p) = 0
@[simp]
theorem cardinal.mk_bool  :
# bool = 2
@[simp]
theorem cardinal.mk_Prop  :
# Prop = 2
@[simp]
theorem cardinal.mk_set {α : Type u} :
# (set α) = 2 ^ # α
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} (h : ∀ ⦃x : α⦄, p xq x) :
@[simp]
theorem cardinal.mk_emptyc (α : Type u) :
theorem cardinal.mk_emptyc_iff {α : Type u} {s : set α} :
# s = 0 s =
@[simp]
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_le_lift {α : Type u} {β : Type v} {f : α → β} :
theorem cardinal.mk_range_eq {α β : Type u} (f : α → β) (h : function.injective f) :
# (set.range f) = # α
theorem cardinal.mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
(# (set.range f)).lift = (# α).lift
theorem cardinal.mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
(# (set.range f)).lift = (# α).lift
theorem cardinal.mk_image_eq {α β : Type u} {f : α → β} {s : set α} (hf : function.injective f) :
# (f '' s) = # s
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 α} (h : ∀ (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 α} :
(s.card) = # s
theorem cardinal.finset_card_lt_omega {α : Type u} (s : finset α) :
theorem cardinal.mk_eq_nat_iff_finset {α : Type u_1} {s : set α} {n : } :
# s = n ∃ (t : finset α), t = s t.card = n
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 α} (H : disjoint S T) :
# (S T) = # S + # T
theorem cardinal.mk_insert {α : Type u} {s : set α} {a : α} (h : a s) :
# (insert a s) = # s + 1
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 α} (h : s t) :
theorem cardinal.mk_subtype_mono {α : Type u} {p q : α → Prop} (h : ∀ (x : α), p xq x) :
# {x // p x} # {x // q x}
theorem cardinal.mk_set_le {α : Type u} (s : set α) :
# s # α
theorem cardinal.mk_union_le_omega {α : Type u_1} {P Q : set α} :
theorem cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : α → β) (s : set α) (h : function.injective f) :
(# (f '' s)).lift = (# s).lift
theorem cardinal.mk_image_eq_of_inj_on_lift {α : Type u} {β : Type v} (f : α → β) (s : set α) (h : set.inj_on f s) :
(# (f '' s)).lift = (# s).lift
theorem cardinal.mk_image_eq_of_inj_on {α β : Type u} (f : α → β) (s : set α) (h : 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 β) (h : function.injective f) :
(# (f ⁻¹' s)).lift (# s).lift
theorem cardinal.mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : set β) (h : 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 β) (h : function.injective f) (h2 : s set.range f) :
(# (f ⁻¹' s)).lift = (# s).lift
theorem cardinal.mk_preimage_of_injective {α β : Type u} (f : α → β) (s : set β) (h : function.injective f) :
theorem cardinal.mk_preimage_of_subset_range {α β : Type u} (f : α → β) (s : set β) (h : s set.range f) :
theorem cardinal.mk_preimage_of_injective_of_subset_range {α β : Type u} (f : α → β) (s : set β) (h : function.injective f) (h2 : s set.range f) :
# (f ⁻¹' s) = # s
theorem cardinal.mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : set α} {t : set β} (h : 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 β} (h : 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 // #s < β } instead of {γ // γ < β}, because the latter lives in a higher universe

Equations
theorem cardinal.powerlt_aux {c c' : cardinal} (h : c < c') :
∃ (s : {s // # s < c'}), # s = c
theorem cardinal.le_powerlt {c₁ c₂ c₃ : cardinal} (h : 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} (h : b c) :
a ^< b a ^< c
theorem cardinal.powerlt_succ {c₁ c₂ : cardinal} (h : c₁ 0) :
c₁ ^< 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} (h : a 0) :
0 ^< a = 1
theorem cardinal.powerlt_zero {a : cardinal} :
a ^< 0 = 0