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

source
@[protected, 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
source
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
source
def cardinal.mk  :
Type u → cardinal

The cardinal number of a type

Equations
source
@[protected]
theorem cardinal.eq {α β : Type u} :
# α = # β ↔ nonempty (α ≃ β)
source
@[simp]
theorem cardinal.mk_def (α : Type u) :
⟦α⟧ = # α
source
@[simp]
theorem cardinal.mk_out (c : cardinal) :
# (quotient.out c) = c
source
@[protected, instance]
def cardinal.has_le  :
has_le cardinal

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

Equations
source
theorem cardinal.le_def (α β : Type u) :
# α ≤ # β ↔ nonempty (α ↪ β)
source
theorem cardinal.mk_le_of_injective {α β : Type u} {f : α → β} (hf : function.injective f) :
# α ≤ # β
source
theorem cardinal.mk_le_of_surjective {α β : Type u} {f : α → β} (hf : function.surjective f) :
# β ≤ # α
source
theorem cardinal.le_mk_iff_exists_set {c : cardinal} {α : Type u} :
c ≤ # α ↔ ∃ (p : set α), # ↥p = c
source
theorem cardinal.out_embedding {c c' : cardinal} :
c ≤ c' ↔ nonempty (quotient.out c ↪ quotient.out c')
source
@[protected]
theorem cardinal.eq_congr {α β : Type u} :
α ≃ β → # α = # β
source
@[protected, instance]
def cardinal.linear_order  :
linear_order cardinal
Equations
source
@[protected, instance]
def cardinal.distrib_lattice  :
distrib_lattice cardinal
Equations
source
@[protected, instance]
def cardinal.has_zero  :
has_zero cardinal
Equations
source
@[protected, instance]
def cardinal.inhabited  :
inhabited cardinal
Equations
source
theorem cardinal.ne_zero_iff_nonempty {α : Type u} :
# α ≠ 0 ↔ nonempty α
source
@[protected, instance]
def cardinal.has_one  :
has_one cardinal
Equations
source
@[protected, instance]
def cardinal.nontrivial  :
nontrivial cardinal
source
theorem cardinal.le_one_iff_subsingleton {α : Type u} :
# α ≤ 1 ↔ subsingleton α
source
theorem cardinal.one_lt_iff_nontrivial {α : Type u} :
1 < # α ↔ nontrivial α
source
@[protected, instance]
def cardinal.has_add  :
has_add cardinal
Equations
source
@[simp]
theorem cardinal.add_def (α β : Type (max u_1 u_2)) :
# α + # β = # (α ⊕ β)
source
@[protected, instance]
def cardinal.has_mul  :
has_mul cardinal
Equations
source
@[simp]
theorem cardinal.mul_def (α β : Type u) :
(# α) * # β = # (α × β)
source
@[protected]
theorem cardinal.eq_zero_or_eq_zero_of_mul_eq_zero {a b : cardinal} :
a * b = 0 → a = 0 ∨ b = 0
source
@[protected, instance]
def cardinal.comm_semiring  :
comm_semiring cardinal
Equations
source
@[protected]
def cardinal.power (a b : cardinal) :
cardinal

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

Equations
source
@[protected, instance]
def cardinal.has_pow  :
has_pow cardinal cardinal
Equations
source
@[simp]
theorem cardinal.power_def (α β : Type u_1) :
# α ^ # β = # (β → α)
source
@[simp]
theorem cardinal.power_zero {a : cardinal} :
a ^ 0 = 1
source
@[simp]
theorem cardinal.power_one {a : cardinal} :
a ^ 1 = a
source
@[simp]
theorem cardinal.one_power {a : cardinal} :
1 ^ a = 1
source
@[simp]
theorem cardinal.prop_eq_two  :
# (ulift Prop) = 2
source
@[simp]
theorem cardinal.zero_power {a : cardinal} :
a ≠ 0 → 0 ^ a = 0
source
theorem cardinal.power_ne_zero {a : cardinal} (b : cardinal) :
a ≠ 0 → a ^ b ≠ 0
source
theorem cardinal.mul_power {a b c : cardinal} :
(a * b) ^ c = (a ^ c) * b ^ c
source
theorem cardinal.power_add {a b c : cardinal} :
a ^ (b + c) = (a ^ b) * a ^ c
source
theorem cardinal.power_mul {a b c : cardinal} :
a ^ b * c = (a ^ b) ^ c
source
@[simp]
theorem cardinal.pow_cast_right (κ : cardinal) (n : ℕ) :
κ ^ ↑n = κ ^ n
source
@[protected]
theorem cardinal.zero_le (a : cardinal) :
0 ≤ a
source
@[protected]
theorem cardinal.add_le_add {a b c d : cardinal} :
a ≤ b → c ≤ d → a + c ≤ b + d
source
@[protected]
theorem cardinal.add_le_add_left (a : cardinal) {b c : cardinal} :
b ≤ c → a + b ≤ a + c
source
@[protected]
theorem cardinal.le_iff_exists_add {a b : cardinal} :
a ≤ b ↔ ∃ (c : cardinal), b = a + c
source
@[protected, instance]
def cardinal.order_bot  :
order_bot cardinal
Equations
source
@[protected, instance]
def cardinal.canonically_ordered_comm_semiring  :
canonically_ordered_comm_semiring cardinal
Equations
source
@[protected, instance]
def cardinal.canonically_linear_ordered_add_monoid  :
canonically_linear_ordered_add_monoid cardinal
Equations
source
@[simp]
theorem cardinal.zero_lt_one  :
0 < 1
source
theorem cardinal.zero_power_le (c : cardinal) :
0 ^ c ≤ 1
source
theorem cardinal.power_le_power_left {a b c : cardinal} :
a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c
source
theorem cardinal.power_le_max_power_one {a b c : cardinal} (h : b ≤ c) :
a ^ b ≤ max (a ^ c) 1
source
theorem cardinal.power_le_power_right {a b c : cardinal} :
a ≤ b → a ^ c ≤ b ^ c
source
theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a
source
@[protected, instance]
def cardinal.no_top_order  :
no_top_order cardinal
source
def cardinal.min {ι : Type u_1} (I : nonempty ι) (f : ι → cardinal) :
cardinal

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

Equations
source
theorem cardinal.min_eq {ι : Type u_1} (I : nonempty ι) (f : ι → cardinal) :
∃ (i : ι), cardinal.min I f = f i
source
theorem cardinal.min_le {ι : Type u_1} {I : nonempty ι} (f : ι → cardinal) (i : ι) :
cardinal.min I f ≤ f i
source
theorem cardinal.le_min {ι : Type u_1} {I : nonempty ι} {f : ι → cardinal} {a : cardinal} :
a ≤ cardinal.min I f ↔ ∀ (i : ι), a ≤ f i
source
@[protected]
theorem cardinal.wf  :
well_founded has_lt.lt
source
@[protected, instance]
def cardinal.has_wf  :
has_well_founded cardinal
Equations
source
@[protected, instance]
def cardinal.wo  :
is_well_order cardinal has_lt.lt
source
def cardinal.succ (c : cardinal) :
cardinal

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
source
theorem cardinal.lt_succ_self (c : cardinal) :
c < c.succ
source
theorem cardinal.succ_le {a b : cardinal} :
a.succ ≤ b ↔ a < b
source
theorem cardinal.lt_succ {a b : cardinal} :
a < b.succ ↔ a ≤ b
source
theorem cardinal.add_one_le_succ (c : cardinal) :
c + 1 ≤ c.succ
source
theorem cardinal.succ_ne_zero (c : cardinal) :
c.succ ≠ 0
source
def cardinal.sum {ι : Type u_1} (f : ι → cardinal) :
cardinal

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

Equations
source
theorem cardinal.le_sum {ι : Type u_1} (f : ι → cardinal) (i : ι) :
f i ≤ cardinal.sum f
source
@[simp]
theorem cardinal.sum_mk {ι : Type u_1} (f : ι → Type u_2) :
cardinal.sum (λ (i : ι), # (f i)) = # (Σ (i : ι), f i)
source
theorem cardinal.sum_const (ι : Type u) (a : cardinal) :
cardinal.sum (λ (_x : ι), a) = (# ι) * a
source
theorem cardinal.sum_le_sum {ι : Type u_1} (f g : ι → cardinal) (H : ∀ (i : ι), f i ≤ g i) :
cardinal.sum f ≤ cardinal.sum g
source
def cardinal.sup {ι : Type u_1} (f : ι → cardinal) :
cardinal

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

Equations
source
theorem cardinal.le_sup {ι : Type u_1} (f : ι → cardinal) (i : ι) :
f i ≤ cardinal.sup f
source
theorem cardinal.sup_le {ι : Type u_1} {f : ι → cardinal} {a : cardinal} :
cardinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
source
theorem cardinal.sup_le_sup {ι : Type u_1} (f g : ι → cardinal) (H : ∀ (i : ι), f i ≤ g i) :
cardinal.sup f ≤ cardinal.sup g
source
theorem cardinal.sup_le_sum {ι : Type u_1} (f : ι → cardinal) :
cardinal.sup f ≤ cardinal.sum f
source
theorem cardinal.sum_le_sup {ι : Type u} (f : ι → cardinal) :
cardinal.sum f ≤ (# ι) * cardinal.sup f
source
theorem cardinal.sup_eq_zero {ι : Type u_1} {f : ι → cardinal} (h : ι → false) :
cardinal.sup f = 0
source
def cardinal.prod {ι : Type u} (f : ι → cardinal) :
cardinal

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

Equations
source
@[simp]
theorem cardinal.prod_mk {ι : Type u_1} (f : ι → Type u_2) :
cardinal.prod (λ (i : ι), # (f i)) = # (Π (i : ι), f i)
source
theorem cardinal.prod_const (ι : Type u) (a : cardinal) :
cardinal.prod (λ (_x : ι), a) = a ^ # ι
source
theorem cardinal.prod_le_prod {ι : Type u_1} (f g : ι → cardinal) (H : ∀ (i : ι), f i ≤ g i) :
cardinal.prod f ≤ cardinal.prod g
source
theorem cardinal.prod_ne_zero {ι : Type u_1} (f : ι → cardinal) :
cardinal.prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
source
theorem cardinal.prod_eq_zero {ι : Type u_1} (f : ι → cardinal) :
cardinal.prod f = 0 ↔ ∃ (i : ι), f i = 0
source
def cardinal.lift (c : cardinal) :
cardinal

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

Equations
source
theorem cardinal.lift_mk (α : Type u) :
(# α).lift = # (ulift α)
source
theorem cardinal.lift_umax  :
cardinal.lift = cardinal.lift
source
theorem cardinal.lift_id' (a : cardinal) :
a.lift = a
source
@[simp]
theorem cardinal.lift_id (a : cardinal) :
a.lift = a
source
@[simp]
theorem cardinal.lift_lift (a : cardinal) :
a.lift.lift = a.lift
source
theorem cardinal.lift_mk_le {α : Type u} {β : Type v} :
(# α).lift ≤ (# β).lift ↔ nonempty (α ↪ β)
source
theorem cardinal.lift_mk_eq {α : Type u} {β : Type v} :
(# α).lift = (# β).lift ↔ nonempty (α ≃ β)
source
@[simp]
theorem cardinal.lift_le {a b : cardinal} :
a.lift ≤ b.lift ↔ a ≤ b
source
@[simp]
theorem cardinal.lift_inj {a b : cardinal} :
a.lift = b.lift ↔ a = b
source
@[simp]
theorem cardinal.lift_lt {a b : cardinal} :
a.lift < b.lift ↔ a < b
source
@[simp]
theorem cardinal.lift_zero  :
0.lift = 0
source
@[simp]
theorem cardinal.lift_one  :
1.lift = 1
source
@[simp]
theorem cardinal.lift_add (a b : cardinal) :
(a + b).lift = a.lift + b.lift
source
@[simp]
theorem cardinal.lift_mul (a b : cardinal) :
(a * b).lift = (a.lift) * b.lift
source
@[simp]
theorem cardinal.lift_power (a b : cardinal) :
(a ^ b).lift = a.lift ^ b.lift
source
@[simp]
theorem cardinal.lift_two_power (a : cardinal) :
(2 ^ a).lift = 2 ^ a.lift
source
@[simp]
theorem cardinal.lift_min {ι : Type u_1} {I : nonempty ι} (f : ι → cardinal) :
(cardinal.min I f).lift = cardinal.min I (cardinal.lift ∘ f)
source
theorem cardinal.lift_down {a : cardinal} {b : cardinal} :
b ≤ a.lift → (∃ (a' : cardinal), a'.lift = b)
source
theorem cardinal.le_lift_iff {a : cardinal} {b : cardinal} :
b ≤ a.lift ↔ ∃ (a' : cardinal), a'.lift = b ∧ a' ≤ a
source
theorem cardinal.lt_lift_iff {a : cardinal} {b : cardinal} :
b < a.lift ↔ ∃ (a' : cardinal), a'.lift = b ∧ a' < a
source
@[simp]
theorem cardinal.lift_succ (a : cardinal) :
a.succ.lift = a.lift.succ
source
@[simp]
theorem cardinal.lift_max {a : cardinal} {b : cardinal} :
a.lift = b.lift ↔ a.lift = b.lift
source
theorem cardinal.mk_prod {α : Type u} {β : Type v} :
# (α × β) = ((# α).lift) * (# β).lift
source
theorem cardinal.sum_const_eq_lift_mul (ι : Type u) (a : cardinal) :
cardinal.sum (λ (_x : ι), a) = ((# ι).lift) * a.lift
source
def cardinal.omega  :
cardinal

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

Equations
source
theorem cardinal.mk_nat  :
# ℕ = cardinal.omega
source
theorem cardinal.omega_ne_zero  :
cardinal.omega ≠ 0
source
theorem cardinal.omega_pos  :
0 < cardinal.omega
source
@[simp]
theorem cardinal.lift_omega  :
cardinal.omega.lift = cardinal.omega
source
@[simp]
theorem cardinal.mk_fin (n : ℕ) :
# (fin n) = ↑n
source
@[simp]
theorem cardinal.lift_nat_cast (n : ℕ) :
↑n.lift = ↑n
source
theorem cardinal.lift_eq_nat_iff {a : cardinal} {n : ℕ} :
a.lift = ↑n ↔ a = ↑n
source
theorem cardinal.nat_eq_lift_eq_iff {n : ℕ} {a : cardinal} :
↑n = a.lift ↔ ↑n = a
source
theorem cardinal.lift_mk_fin (n : ℕ) :
(# (fin n)).lift = ↑n
source
theorem cardinal.fintype_card (α : Type u) [fintype α] :
# α = ↑(fintype.card α)
source
theorem cardinal.card_le_of_finset {α : Type u_1} (s : finset α) :
↑(s.card) ≤ # α
source
@[simp, norm_cast]
theorem cardinal.nat_cast_pow {m n : ℕ} :
↑(m ^ n) = ↑m ^ ↑n
source
@[simp, norm_cast]
theorem cardinal.nat_cast_le {m n : ℕ} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp, norm_cast]
theorem cardinal.nat_cast_lt {m n : ℕ} :
↑m < ↑n ↔ m < n
source
@[simp, norm_cast]
theorem cardinal.nat_cast_inj {m n : ℕ} :
↑m = ↑n ↔ m = n
source
@[simp, norm_cast]
theorem cardinal.nat_succ (n : ℕ) :
↑(n.succ) = ↑n.succ
source
@[simp]
theorem cardinal.succ_zero  :
0.succ = 1
source
theorem cardinal.card_le_of {α : Type u} {n : ℕ} (H : ∀ (s : finset α), s.card ≤ n) :
# α ≤ ↑n
source
theorem cardinal.cantor' (a : cardinal) {b : cardinal} (hb : 1 < b) :
a < b ^ a
source
theorem cardinal.one_le_iff_pos {c : cardinal} :
1 ≤ c ↔ 0 < c
source
theorem cardinal.one_le_iff_ne_zero {c : cardinal} :
1 ≤ c ↔ c ≠ 0
source
theorem cardinal.nat_lt_omega (n : ℕ) :
↑n < cardinal.omega
source
@[simp]
theorem cardinal.one_lt_omega  :
1 < cardinal.omega
source
theorem cardinal.lt_omega {c : cardinal} :
c < cardinal.omega ↔ ∃ (n : ℕ), c = ↑n
source
theorem cardinal.omega_le {c : cardinal} :
cardinal.omega ≤ c ↔ ∀ (n : ℕ), ↑n ≤ c
source
theorem cardinal.lt_omega_iff_fintype {α : Type u} :
# α < cardinal.omega ↔ nonempty (fintype α)
source
theorem cardinal.lt_omega_iff_finite {α : Type u_1} {S : set α} :
# ↥S < cardinal.omega ↔ S.finite
source
@[protected, instance]
def cardinal.can_lift_cardinal_nat  :
can_lift cardinal ℕ
Equations
source
theorem cardinal.add_lt_omega {a b : cardinal} (ha : a < cardinal.omega) (hb : b < cardinal.omega) :
a + b < cardinal.omega
source
theorem cardinal.add_lt_omega_iff {a b : cardinal} :
a + b < cardinal.omega ↔ a < cardinal.omega ∧ b < cardinal.omega
source
theorem cardinal.mul_lt_omega {a b : cardinal} (ha : a < cardinal.omega) (hb : b < cardinal.omega) :
a * b < cardinal.omega
source
theorem cardinal.mul_lt_omega_iff {a b : cardinal} :
a * b < cardinal.omega ↔ a = 0 ∨ b = 0 ∨ a < cardinal.omega ∧ b < cardinal.omega
source
theorem cardinal.mul_lt_omega_iff_of_ne_zero {a b : cardinal} (ha : a ≠ 0) (hb : b ≠ 0) :
a * b < cardinal.omega ↔ a < cardinal.omega ∧ b < cardinal.omega
source
theorem cardinal.power_lt_omega {a b : cardinal} (ha : a < cardinal.omega) (hb : b < cardinal.omega) :
a ^ b < cardinal.omega
source
theorem cardinal.eq_one_iff_subsingleton_and_nonempty {α : Type u_1} :
# α = 1 ↔ subsingleton α ∧ nonempty α
source
theorem cardinal.infinite_iff {α : Type u} :
infinite α ↔ cardinal.omega ≤ # α
source
theorem cardinal.denumerable_iff {α : Type u} :
nonempty (denumerable α) ↔ # α = cardinal.omega
source
theorem cardinal.countable_iff {α : Type u} (s : set α) :
s.countable ↔ # ↥s ≤ cardinal.omega
source
def cardinal.to_nat  :
zero_hom cardinal ℕ

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

Equations
source
theorem cardinal.to_nat_apply_of_lt_omega {c : cardinal} (h : c < cardinal.omega) :
⇑cardinal.to_nat c = classical.some _
source
@[simp]
theorem cardinal.to_nat_apply_of_omega_le {c : cardinal} (h : cardinal.omega ≤ c) :
⇑cardinal.to_nat c = 0
source
@[simp]
theorem cardinal.cast_to_nat_of_lt_omega {c : cardinal} (h : c < cardinal.omega) :
↑(⇑cardinal.to_nat c) = c
source
@[simp]
theorem cardinal.to_nat_cast (n : ℕ) :
⇑cardinal.to_nat ↑n = n
source
theorem cardinal.to_nat_right_inverse  :
function.right_inverse coe ⇑cardinal.to_nat

to_nat has a right-inverse: coercion.

source
theorem cardinal.to_nat_surjective  :
function.surjective ⇑cardinal.to_nat
source
@[simp]
theorem cardinal.mk_to_nat_of_infinite {α : Type u} [h : infinite α] :
⇑cardinal.to_nat (# α) = 0
source
@[simp]
theorem cardinal.mk_to_nat_eq_card {α : Type u} [fintype α] :
⇑cardinal.to_nat (# α) = fintype.card α
source
@[simp]
theorem cardinal.zero_to_nat  :
⇑cardinal.to_nat 0 = 0
source
@[simp]
theorem cardinal.one_to_nat  :
⇑cardinal.to_nat 1 = 1
source
def cardinal.to_enat  :
cardinal →+ enat

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

Equations
source
@[simp]
theorem cardinal.to_enat_apply_of_lt_omega {c : cardinal} (h : c < cardinal.omega) :
⇑cardinal.to_enat c = ↑(⇑cardinal.to_nat c)
source
@[simp]
theorem cardinal.to_enat_apply_of_omega_le {c : cardinal} (h : cardinal.omega ≤ c) :
⇑cardinal.to_enat c = ⊤
source
@[simp]
theorem cardinal.to_enat_cast (n : ℕ) :
⇑cardinal.to_enat ↑n = ↑n
source
@[simp]
theorem cardinal.mk_to_enat_of_infinite {α : Type u} [h : infinite α] :
⇑cardinal.to_enat (# α) = ⊤
source
theorem cardinal.to_enat_surjective  :
function.surjective ⇑cardinal.to_enat
source
@[simp]
theorem cardinal.mk_to_enat_eq_coe_card {α : Type u} [fintype α] :
⇑cardinal.to_enat (# α) = ↑(fintype.card α)
source
theorem cardinal.mk_int  :
# ℤ = cardinal.omega
source
theorem cardinal.mk_pnat  :
# ℕ+ = cardinal.omega
source
theorem cardinal.two_le_iff {α : Type u} :
2 ≤ # α ↔ ∃ (x y : α), x ≠ y
source
theorem cardinal.two_le_iff' {α : Type u} (x : α) :
2 ≤ # α ↔ ∃ (y : α), x ≠ y
source
theorem cardinal.sum_lt_prod {ι : Type u_1} (f g : ι → cardinal) (H : ∀ (i : ι), f i < g i) :
cardinal.sum f < cardinal.prod g

König's theorem

source
@[simp]
theorem cardinal.mk_empty  :
# empty = 0
source
@[simp]
theorem cardinal.mk_pempty  :
# pempty = 0
source
@[simp]
theorem cardinal.mk_plift_of_false {p : Prop} (h : ¬p) :
# (plift p) = 0
source
theorem cardinal.mk_unit  :
# unit = 1
source
@[simp]
theorem cardinal.mk_punit  :
# punit = 1
source
@[simp]
theorem cardinal.mk_singleton {α : Type u} (x : α) :
# ↥{x} = 1
source
@[simp]
theorem cardinal.mk_plift_of_true {p : Prop} (h : p) :
# (plift p) = 1
source
@[simp]
theorem cardinal.mk_bool  :
# bool = 2
source
@[simp]
theorem cardinal.mk_Prop  :
# Prop = 2
source
@[simp]
theorem cardinal.mk_set {α : Type u} :
# (set α) = 2 ^ # α
source
@[simp]
theorem cardinal.mk_option {α : Type u} :
# (option α) = # α + 1
source
theorem cardinal.mk_list_eq_sum_pow (α : Type u) :
# (list α) = cardinal.sum (λ (n : ℕ), # α ^ ↑n)
source
theorem cardinal.mk_quot_le {α : Type u} {r : α → α → Prop} :
# (quot r) ≤ # α
source
theorem cardinal.mk_quotient_le {α : Type u} {s : setoid α} :
# (quotient s) ≤ # α
source
theorem cardinal.mk_subtype_le {α : Type u} (p : α → Prop) :
# (subtype p) ≤ # α
source
theorem cardinal.mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x : α⦄, p x → q x) :
# (subtype p) ≤ # (subtype q)
source
@[simp]
theorem cardinal.mk_emptyc (α : Type u) :
# ↥∅ = 0
source
theorem cardinal.mk_emptyc_iff {α : Type u} {s : set α} :
# ↥s = 0 ↔ s = ∅
source
theorem cardinal.mk_univ {α : Type u} :
# ↥set.univ = # α
source
theorem cardinal.mk_image_le {α β : Type u} {f : α → β} {s : set α} :
# ↥(f '' s) ≤ # ↥s
source
theorem cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(# ↥(f '' s)).lift ≤ (# ↥s).lift
source
theorem cardinal.mk_range_le {α β : Type u} {f : α → β} :
# ↥(set.range f) ≤ # α
source
theorem cardinal.mk_range_eq {α β : Type u} (f : α → β) (h : function.injective f) :
# ↥(set.range f) = # α
source
theorem cardinal.mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
(# ↥(set.range f)).lift = (# α).lift
source
theorem cardinal.mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
(# ↥(set.range f)).lift = (# α).lift
source
theorem cardinal.mk_image_eq {α β : Type u} {f : α → β} {s : set α} (hf : function.injective f) :
# ↥(f '' s) = # ↥s
source
theorem cardinal.mk_Union_le_sum_mk {α ι : Type u} {f : ι → set α} :
# (↥⋃ (i : ι), f i) ≤ cardinal.sum (λ (i : ι), # ↥(f i))
source
theorem cardinal.mk_Union_eq_sum_mk {α ι : Type u} {f : ι → set α} (h : ∀ (i j : ι), i ≠ j → disjoint (f i) (f j)) :
# (↥⋃ (i : ι), f i) = cardinal.sum (λ (i : ι), # ↥(f i))
source
theorem cardinal.mk_Union_le {α ι : Type u} (f : ι → set α) :
# (↥⋃ (i : ι), f i) ≤ (# ι) * cardinal.sup (λ (i : ι), # ↥(f i))
source
theorem cardinal.mk_sUnion_le {α : Type u} (A : set (set α)) :
# (↥⋃₀A) ≤ (# ↥A) * cardinal.sup (λ (s : ↥A), # ↥s)
source
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))
source
@[simp]
theorem cardinal.finset_card {α : Type u} {s : finset α} :
↑(s.card) = # ↥↑s
source
theorem cardinal.finset_card_lt_omega {α : Type u} (s : finset α) :
# ↥↑s < cardinal.omega
source
theorem cardinal.mk_eq_nat_iff_finset {α : Type u_1} {s : set α} {n : ℕ} :
# ↥s = ↑n ↔ ∃ (t : finset α), ↑t = s ∧ t.card = n
source
theorem cardinal.mk_union_add_mk_inter {α : Type u} {S T : set α} :
# ↥(S ∪ T) + # ↥(S ∩ T) = # ↥S + # ↥T
source
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.

source
theorem cardinal.mk_union_of_disjoint {α : Type u} {S T : set α} (H : disjoint S T) :
# ↥(S ∪ T) = # ↥S + # ↥T
source
theorem cardinal.mk_sum_compl {α : Type u_1} (s : set α) :
# ↥s + # ↥sᶜ = # α
source
theorem cardinal.mk_le_mk_of_subset {α : Type u_1} {s t : set α} (h : s ⊆ t) :
# ↥s ≤ # ↥t
source
theorem cardinal.mk_subtype_mono {α : Type u} {p q : α → Prop} (h : ∀ (x : α), p x → q x) :
# {x // p x} ≤ # {x // q x}
source
theorem cardinal.mk_set_le {α : Type u} (s : set α) :
# ↥s ≤ # α
source
theorem cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : α → β) (s : set α) (h : function.injective f) :
(# ↥(f '' s)).lift = (# ↥s).lift
source
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
source
theorem cardinal.mk_image_eq_of_inj_on {α β : Type u} (f : α → β) (s : set α) (h : set.inj_on f s) :
# ↥(f '' s) = # ↥s
source
theorem cardinal.mk_subtype_of_equiv {α β : Type u} (p : β → Prop) (e : α ≃ β) :
# {a // p (⇑e a)} = # {b // p b}
source
theorem cardinal.mk_sep {α : Type u} (s : set α) (t : α → Prop) :
# ↥{x ∈ s | t x} = # ↥{x : ↥s | t x.val}
source
theorem cardinal.mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : set β) (h : function.injective f) :
(# ↥(f ⁻¹' s)).lift ≤ (# ↥s).lift
source
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
source
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
source
theorem cardinal.mk_preimage_of_injective {α β : Type u} (f : α → β) (s : set β) (h : function.injective f) :
# ↥(f ⁻¹' s) ≤ # ↥s
source
theorem cardinal.mk_preimage_of_subset_range {α β : Type u} (f : α → β) (s : set β) (h : s ⊆ set.range f) :
# ↥s ≤ # ↥(f ⁻¹' s)
source
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
source
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
source
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}
source
theorem cardinal.le_mk_iff_exists_subset {c : cardinal} {α : Type u} {s : set α} :
c ≤ # ↥s ↔ ∃ (p : set α), p ⊆ s ∧ # ↥p = c
source
def cardinal.powerlt (α β : cardinal) :
cardinal

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
source
theorem cardinal.powerlt_aux {c c' : cardinal} (h : c < c') :
∃ (s : {s // # ↥s < c'}), # ↥s = c
source
theorem cardinal.le_powerlt {c₁ c₂ c₃ : cardinal} (h : c₂ < c₃) :
c₁ ^ c₂ ≤ c₁ ^< c₃
source
theorem cardinal.powerlt_le {c₁ c₂ c₃ : cardinal} :
c₁ ^< c₂ ≤ c₃ ↔ ∀ (c₄ : cardinal), c₄ < c₂ → c₁ ^ c₄ ≤ c₃
source
theorem cardinal.powerlt_le_powerlt_left {a b c : cardinal} (h : b ≤ c) :
a ^< b ≤ a ^< c
source
theorem cardinal.powerlt_succ {c₁ c₂ : cardinal} (h : c₁ ≠ 0) :
c₁ ^< c₂.succ = c₁ ^ c₂
source
theorem cardinal.powerlt_max {c₁ c₂ c₃ : cardinal} :
c₁ ^< max c₂ c₃ = max (c₁ ^< c₂) (c₁ ^< c₃)
source
theorem cardinal.zero_powerlt {a : cardinal} (h : a ≠ 0) :
0 ^< a = 1
source
theorem cardinal.powerlt_zero {a : cardinal} :
a ^< 0 = 0
source
theorem equiv.cardinal_eq {α β : Type u_1} :
α ≃ β → # α = # β