mathlib3 documentation

set_theory.cardinal.ordinal

Cardinals and ordinals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Relationships between cardinals and ordinals, properties of cardinals that are proved using ordinals.

Main definitions #

Main Statements #

Tags #

cardinal arithmetic (for infinite cardinals)

source
theorem cardinal.ord_is_limit {c : cardinal} (co : cardinal.aleph_0 ≤ c) :
c.ord.is_limit

Aleph cardinals #

source
noncomputable def cardinal.aleph_idx.initial_seg  :
initial_seg has_lt.lt has_lt.lt

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So aleph_idx n = n, aleph_idx ω = ω, aleph_idx ℵ₁ = ω + 1 and so on.) In this definition, we register additionally that this function is an initial segment, i.e., it is order preserving and its range is an initial segment of the ordinals. For the basic function version, see aleph_idx. For an upgraded version stating that the range is everything, see aleph_idx.rel_iso.

Equations
source
noncomputable def cardinal.aleph_idx  :
cardinal → ordinal

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So aleph_idx n = n, aleph_idx ω = ω, aleph_idx ℵ₁ = ω + 1 and so on.) For an upgraded version stating that the range is everything, see aleph_idx.rel_iso.

Equations
source
@[simp]
theorem cardinal.aleph_idx.initial_seg_coe  :
⇑cardinal.aleph_idx.initial_seg = cardinal.aleph_idx
source
@[simp]
theorem cardinal.aleph_idx_lt {a b : cardinal} :
a.aleph_idx < b.aleph_idx ↔ a < b
source
@[simp]
theorem cardinal.aleph_idx_le {a b : cardinal} :
a.aleph_idx ≤ b.aleph_idx ↔ a ≤ b
source
theorem cardinal.aleph_idx.init {a : cardinal} {b : ordinal} :
b < a.aleph_idx → (∃ (c : cardinal), c.aleph_idx = b)
source
noncomputable def cardinal.aleph_idx.rel_iso  :
has_lt.lt ≃r has_lt.lt

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So aleph_idx n = n, aleph_idx ℵ₀ = ω, aleph_idx ℵ₁ = ω + 1 and so on.) In this version, we register additionally that this function is an order isomorphism between cardinals and ordinals. For the basic function version, see aleph_idx.

Equations
source
@[simp]
theorem cardinal.aleph_idx.rel_iso_coe  :
⇑cardinal.aleph_idx.rel_iso = cardinal.aleph_idx
source
@[simp]
theorem cardinal.type_cardinal  :
ordinal.type has_lt.lt = ordinal.univ
source
@[simp]
theorem cardinal.mk_cardinal  :
cardinal.mk cardinal = cardinal.univ
source
noncomputable def cardinal.aleph'.rel_iso  :
has_lt.lt ≃r has_lt.lt

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc. In this version, we register additionally that this function is an order isomorphism between ordinals and cardinals. For the basic function version, see aleph'.

Equations
source
noncomputable def cardinal.aleph'  :
ordinal → cardinal

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc.

Equations
source
@[simp]
theorem cardinal.aleph'.rel_iso_coe  :
⇑cardinal.aleph'.rel_iso = cardinal.aleph'
source
@[simp]
theorem cardinal.aleph'_lt {o₁ o₂ : ordinal} :
cardinal.aleph' o₁ < cardinal.aleph' o₂ ↔ o₁ < o₂
source
@[simp]
theorem cardinal.aleph'_le {o₁ o₂ : ordinal} :
cardinal.aleph' o₁ ≤ cardinal.aleph' o₂ ↔ o₁ ≤ o₂
source
@[simp]
theorem cardinal.aleph'_aleph_idx (c : cardinal) :
cardinal.aleph' c.aleph_idx = c
source
@[simp]
theorem cardinal.aleph_idx_aleph' (o : ordinal) :
(cardinal.aleph' o).aleph_idx = o
source
@[simp]
theorem cardinal.aleph'_zero  :
cardinal.aleph' 0 = 0
source
@[simp]
theorem cardinal.aleph'_succ {o : ordinal} :
cardinal.aleph' (order.succ o) = order.succ (cardinal.aleph' o)
source
@[simp]
theorem cardinal.aleph'_nat (n : ℕ) :
cardinal.aleph' ↑n = ↑n
source
theorem cardinal.aleph'_le_of_limit {o : ordinal} (l : o.is_limit) {c : cardinal} :
cardinal.aleph' o ≤ c ↔ ∀ (o' : ordinal), o' < o → cardinal.aleph' o' ≤ c
source
theorem cardinal.aleph'_limit {o : ordinal} (ho : o.is_limit) :
cardinal.aleph' o = ⨆ (a : ↥(set.Iio o)), cardinal.aleph' ↑a
source
@[simp]
theorem cardinal.aleph'_omega  :
cardinal.aleph' ordinal.omega = cardinal.aleph_0
source
@[simp]
noncomputable def cardinal.aleph'_equiv  :
ordinal ≃ cardinal

aleph' and aleph_idx form an equivalence between ordinal and cardinal

Equations
source
noncomputable def cardinal.aleph (o : ordinal) :
cardinal

The aleph function gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on.

Equations
source
@[simp]
theorem cardinal.aleph_lt {o₁ o₂ : ordinal} :
cardinal.aleph o₁ < cardinal.aleph o₂ ↔ o₁ < o₂
source
@[simp]
theorem cardinal.aleph_le {o₁ o₂ : ordinal} :
cardinal.aleph o₁ ≤ cardinal.aleph o₂ ↔ o₁ ≤ o₂
source
@[simp]
theorem cardinal.max_aleph_eq (o₁ o₂ : ordinal) :
linear_order.max (cardinal.aleph o₁) (cardinal.aleph o₂) = cardinal.aleph (linear_order.max o₁ o₂)
source
@[simp]
theorem cardinal.aleph_succ {o : ordinal} :
cardinal.aleph (order.succ o) = order.succ (cardinal.aleph o)
source
@[simp]
theorem cardinal.aleph_zero  :
cardinal.aleph 0 = cardinal.aleph_0
source
theorem cardinal.aleph_limit {o : ordinal} (ho : o.is_limit) :
cardinal.aleph o = ⨆ (a : ↥(set.Iio o)), cardinal.aleph ↑a
source
theorem cardinal.aleph_0_le_aleph' {o : ordinal} :
cardinal.aleph_0 ≤ cardinal.aleph' o ↔ ordinal.omega ≤ o
source
theorem cardinal.aleph_0_le_aleph (o : ordinal) :
cardinal.aleph_0 ≤ cardinal.aleph o
source
theorem cardinal.aleph'_pos {o : ordinal} (ho : 0 < o) :
0 < cardinal.aleph' o
source
theorem cardinal.aleph_pos (o : ordinal) :
0 < cardinal.aleph o
source
@[simp]
theorem cardinal.aleph_to_nat (o : ordinal) :
⇑cardinal.to_nat (cardinal.aleph o) = 0
source
@[simp]
theorem cardinal.aleph_to_part_enat (o : ordinal) :
⇑cardinal.to_part_enat (cardinal.aleph o) = ⊤
source
@[protected, instance]
def cardinal.nonempty_out_aleph (o : ordinal) :
nonempty (quotient.out (cardinal.aleph o).ord).α
source
theorem cardinal.ord_aleph_is_limit (o : ordinal) :
(cardinal.aleph o).ord.is_limit
source
@[protected, instance]
def cardinal.α.no_max_order (o : ordinal) :
no_max_order (quotient.out (cardinal.aleph o).ord).α
source
theorem cardinal.exists_aleph {c : cardinal} :
cardinal.aleph_0 ≤ c ↔ ∃ (o : ordinal), c = cardinal.aleph o
source
theorem cardinal.aleph'_is_normal  :
ordinal.is_normal (cardinal.ord ∘ cardinal.aleph')
source
theorem cardinal.aleph_is_normal  :
ordinal.is_normal (cardinal.ord ∘ cardinal.aleph)
source
theorem cardinal.succ_aleph_0  :
order.succ cardinal.aleph_0 = cardinal.aleph 1
source
theorem cardinal.aleph_0_lt_aleph_one  :
cardinal.aleph_0 < cardinal.aleph 1
source
theorem cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : set α) :
s.countable ↔ cardinal.mk ↥s < cardinal.aleph 1
source
theorem cardinal.ord_card_unbounded  :
set.unbounded has_lt.lt {b : ordinal | b.card.ord = b}

Ordinals that are cardinals are unbounded.

source
theorem cardinal.eq_aleph'_of_eq_card_ord {o : ordinal} (ho : o.card.ord = o) :
∃ (a : ordinal), (cardinal.aleph' a).ord = o
source
theorem cardinal.ord_aleph'_eq_enum_card  :
cardinal.ord ∘ cardinal.aleph' = ordinal.enum_ord {b : ordinal | b.card.ord = b}

ord ∘ aleph' enumerates the ordinals that are cardinals.

source
theorem cardinal.ord_card_unbounded'  :
set.unbounded has_lt.lt {b : ordinal | b.card.ord = b ∧ ordinal.omega ≤ b}

Infinite ordinals that are cardinals are unbounded.

source
theorem cardinal.eq_aleph_of_eq_card_ord {o : ordinal} (ho : o.card.ord = o) (ho' : ordinal.omega ≤ o) :
∃ (a : ordinal), (cardinal.aleph a).ord = o
source
theorem cardinal.ord_aleph_eq_enum_card  :
cardinal.ord ∘ cardinal.aleph = ordinal.enum_ord {b : ordinal | b.card.ord = b ∧ ordinal.omega ≤ b}

ord ∘ aleph enumerates the infinite ordinals that are cardinals.

Beth cardinals #

source
noncomputable def cardinal.beth (o : ordinal) :
cardinal

Beth numbers are defined so that beth 0 = ℵ₀, beth (succ o) = 2 ^ (beth o), and when o is a limit ordinal, beth o is the supremum of beth o' for o' < o.

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, beth o = aleph o for every o.

Equations
source
@[simp]
theorem cardinal.beth_zero  :
cardinal.beth 0 = cardinal.aleph_0
source
@[simp]
theorem cardinal.beth_succ (o : ordinal) :
cardinal.beth (order.succ o) = 2 ^ cardinal.beth o
source
theorem cardinal.beth_limit {o : ordinal} :
o.is_limit → (cardinal.beth o = ⨆ (a : ↥(set.Iio o)), cardinal.beth ↑a)
source
theorem cardinal.beth_strict_mono  :
strict_mono cardinal.beth
source
theorem cardinal.beth_mono  :
monotone cardinal.beth
source
@[simp]
theorem cardinal.beth_lt {o₁ o₂ : ordinal} :
cardinal.beth o₁ < cardinal.beth o₂ ↔ o₁ < o₂
source
@[simp]
theorem cardinal.beth_le {o₁ o₂ : ordinal} :
cardinal.beth o₁ ≤ cardinal.beth o₂ ↔ o₁ ≤ o₂
source
theorem cardinal.aleph_le_beth (o : ordinal) :
cardinal.aleph o ≤ cardinal.beth o
source
theorem cardinal.aleph_0_le_beth (o : ordinal) :
cardinal.aleph_0 ≤ cardinal.beth o
source
theorem cardinal.beth_pos (o : ordinal) :
0 < cardinal.beth o
source
theorem cardinal.beth_ne_zero (o : ordinal) :
cardinal.beth o ≠ 0
source
theorem cardinal.beth_normal  :
ordinal.is_normal (λ (o : ordinal), (cardinal.beth o).ord)

Properties of mul #

source
theorem cardinal.mul_eq_self {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
c * c = c

If α is an infinite type, then α × α and α have the same cardinality.

source
theorem cardinal.mul_eq_max {a b : cardinal} (ha : cardinal.aleph_0 ≤ a) (hb : cardinal.aleph_0 ≤ b) :
a * b = linear_order.max a b

If α and β are infinite types, then the cardinality of α × β is the maximum of the cardinalities of α and β.

source
@[simp]
theorem cardinal.mul_mk_eq_max {α β : Type u_1} [infinite α] [infinite β] :
cardinal.mk α * cardinal.mk β = linear_order.max (cardinal.mk α) (cardinal.mk β)
source
@[simp]
theorem cardinal.aleph_mul_aleph (o₁ o₂ : ordinal) :
cardinal.aleph o₁ * cardinal.aleph o₂ = cardinal.aleph (linear_order.max o₁ o₂)
source
@[simp]
theorem cardinal.aleph_0_mul_eq {a : cardinal} (ha : cardinal.aleph_0 ≤ a) :
cardinal.aleph_0 * a = a
source
@[simp]
theorem cardinal.mul_aleph_0_eq {a : cardinal} (ha : cardinal.aleph_0 ≤ a) :
a * cardinal.aleph_0 = a
source
@[simp]
theorem cardinal.aleph_0_mul_mk_eq {α : Type u_1} [infinite α] :
cardinal.aleph_0 * cardinal.mk α = cardinal.mk α
source
@[simp]
theorem cardinal.mk_mul_aleph_0_eq {α : Type u_1} [infinite α] :
cardinal.mk α * cardinal.aleph_0 = cardinal.mk α
source
@[simp]
theorem cardinal.aleph_0_mul_aleph (o : ordinal) :
cardinal.aleph_0 * cardinal.aleph o = cardinal.aleph o
source
@[simp]
theorem cardinal.aleph_mul_aleph_0 (o : ordinal) :
cardinal.aleph o * cardinal.aleph_0 = cardinal.aleph o
source
theorem cardinal.mul_lt_of_lt {a b c : cardinal} (hc : cardinal.aleph_0 ≤ c) (h1 : a < c) (h2 : b < c) :
a * b < c
source
theorem cardinal.mul_le_max_of_aleph_0_le_left {a b : cardinal} (h : cardinal.aleph_0 ≤ a) :
a * b ≤ linear_order.max a b
source
theorem cardinal.mul_eq_max_of_aleph_0_le_left {a b : cardinal} (h : cardinal.aleph_0 ≤ a) (h' : b ≠ 0) :
a * b = linear_order.max a b
source
theorem cardinal.mul_le_max_of_aleph_0_le_right {a b : cardinal} (h : cardinal.aleph_0 ≤ b) :
a * b ≤ linear_order.max a b
source
theorem cardinal.mul_eq_max_of_aleph_0_le_right {a b : cardinal} (h' : a ≠ 0) (h : cardinal.aleph_0 ≤ b) :
a * b = linear_order.max a b
source
theorem cardinal.mul_eq_max' {a b : cardinal} (h : cardinal.aleph_0 ≤ a * b) :
a * b = linear_order.max a b
source
theorem cardinal.mul_le_max (a b : cardinal) :
a * b ≤ linear_order.max (linear_order.max a b) cardinal.aleph_0
source
theorem cardinal.mul_eq_left {a b : cardinal} (ha : cardinal.aleph_0 ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) :
a * b = a
source
theorem cardinal.mul_eq_right {a b : cardinal} (hb : cardinal.aleph_0 ≤ b) (ha : a ≤ b) (ha' : a ≠ 0) :
a * b = b
source
theorem cardinal.le_mul_left {a b : cardinal} (h : b ≠ 0) :
a ≤ b * a
source
theorem cardinal.le_mul_right {a b : cardinal} (h : b ≠ 0) :
a ≤ a * b
source
theorem cardinal.mul_eq_left_iff {a b : cardinal} :
a * b = a ↔ linear_order.max cardinal.aleph_0 b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Properties of add #

source
theorem cardinal.add_eq_self {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
c + c = c

If α is an infinite type, then α ⊕ α and α have the same cardinality.

source
theorem cardinal.add_eq_max {a b : cardinal} (ha : cardinal.aleph_0 ≤ a) :
a + b = linear_order.max a b

If α is an infinite type, then the cardinality of α ⊕ β is the maximum of the cardinalities of α and β.

source
theorem cardinal.add_eq_max' {a b : cardinal} (ha : cardinal.aleph_0 ≤ b) :
a + b = linear_order.max a b
source
@[simp]
theorem cardinal.add_mk_eq_max {α β : Type u_1} [infinite α] :
cardinal.mk α + cardinal.mk β = linear_order.max (cardinal.mk α) (cardinal.mk β)
source
@[simp]
theorem cardinal.add_mk_eq_max' {α β : Type u_1} [infinite β] :
cardinal.mk α + cardinal.mk β = linear_order.max (cardinal.mk α) (cardinal.mk β)
source
theorem cardinal.add_le_max (a b : cardinal) :
a + b ≤ linear_order.max (linear_order.max a b) cardinal.aleph_0
source
theorem cardinal.add_le_of_le {a b c : cardinal} (hc : cardinal.aleph_0 ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) :
a + b ≤ c
source
theorem cardinal.add_lt_of_lt {a b c : cardinal} (hc : cardinal.aleph_0 ≤ c) (h1 : a < c) (h2 : b < c) :
a + b < c
source
theorem cardinal.eq_of_add_eq_of_aleph_0_le {a b c : cardinal} (h : a + b = c) (ha : a < c) (hc : cardinal.aleph_0 ≤ c) :
b = c
source
theorem cardinal.add_eq_left {a b : cardinal} (ha : cardinal.aleph_0 ≤ a) (hb : b ≤ a) :
a + b = a
source
theorem cardinal.add_eq_right {a b : cardinal} (hb : cardinal.aleph_0 ≤ b) (ha : a ≤ b) :
a + b = b
source
theorem cardinal.add_eq_left_iff {a b : cardinal} :
a + b = a ↔ linear_order.max cardinal.aleph_0 b ≤ a ∨ b = 0
source
theorem cardinal.add_eq_right_iff {a b : cardinal} :
a + b = b ↔ linear_order.max cardinal.aleph_0 a ≤ b ∨ a = 0
source
theorem cardinal.add_nat_eq {a : cardinal} (n : ℕ) (ha : cardinal.aleph_0 ≤ a) :
a + ↑n = a
source
theorem cardinal.add_one_eq {a : cardinal} (ha : cardinal.aleph_0 ≤ a) :
a + 1 = a
source
@[simp]
theorem cardinal.mk_add_one_eq {α : Type u_1} [infinite α] :
cardinal.mk α + 1 = cardinal.mk α
source
@[protected]
theorem cardinal.eq_of_add_eq_add_left {a b c : cardinal} (h : a + b = a + c) (ha : a < cardinal.aleph_0) :
b = c
source
@[protected]
theorem cardinal.eq_of_add_eq_add_right {a b c : cardinal} (h : a + b = c + b) (hb : b < cardinal.aleph_0) :
a = c
source
@[simp]
theorem cardinal.aleph_add_aleph (o₁ o₂ : ordinal) :
cardinal.aleph o₁ + cardinal.aleph o₂ = cardinal.aleph (linear_order.max o₁ o₂)
source
theorem cardinal.principal_add_ord {c : cardinal} (hc : cardinal.aleph_0 ≤ c) :
ordinal.principal has_add.add c.ord
source
theorem cardinal.principal_add_aleph (o : ordinal) :
ordinal.principal has_add.add (cardinal.aleph o).ord
source
theorem cardinal.add_right_inj_of_lt_aleph_0 {α β γ : cardinal} (γ₀ : γ < cardinal.aleph_0) :
α + γ = β + γ ↔ α = β
source
@[simp]
theorem cardinal.add_nat_inj {α β : cardinal} (n : ℕ) :
α + ↑n = β + ↑n ↔ α = β
source
@[simp]
theorem cardinal.add_one_inj {α β : cardinal} :
α + 1 = β + 1 ↔ α = β
source
theorem cardinal.add_le_add_iff_of_lt_aleph_0 {α β γ : cardinal} (γ₀ : γ < cardinal.aleph_0) :
α + γ ≤ β + γ ↔ α ≤ β
source
@[simp]
theorem cardinal.add_nat_le_add_nat_iff_of_lt_aleph_0 {α β : cardinal} (n : ℕ) :
α + ↑n ≤ β + ↑n ↔ α ≤ β
source
@[simp]
theorem cardinal.add_one_le_add_one_iff_of_lt_aleph_0 {α β : cardinal} :
α + 1 ≤ β + 1 ↔ α ≤ β

Properties about power #

source
theorem cardinal.pow_le {κ μ : cardinal} (H1 : cardinal.aleph_0 ≤ κ) (H2 : μ < cardinal.aleph_0) :
κ ^ μ ≤ κ
source
theorem cardinal.pow_eq {κ μ : cardinal} (H1 : cardinal.aleph_0 ≤ κ) (H2 : 1 ≤ μ) (H3 : μ < cardinal.aleph_0) :
κ ^ μ = κ
source
theorem cardinal.power_self_eq {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
c ^ c = 2 ^ c
source
theorem cardinal.prod_eq_two_power {ι : Type u} [infinite ι] {c : ι → cardinal} (h₁ : ∀ (i : ι), 2 ≤ c i) (h₂ : ∀ (i : ι), (c i).lift ≤ (cardinal.mk ι).lift) :
cardinal.prod c = 2 ^ (cardinal.mk ι).lift
source
theorem cardinal.power_eq_two_power {c₁ c₂ : cardinal} (h₁ : cardinal.aleph_0 ≤ c₁) (h₂ : 2 ≤ c₂) (h₂' : c₂ ≤ c₁) :
c₂ ^ c₁ = 2 ^ c₁
source
theorem cardinal.nat_power_eq {c : cardinal} (h : cardinal.aleph_0 ≤ c) {n : ℕ} (hn : 2 ≤ n) :
↑n ^ c = 2 ^ c
source
theorem cardinal.power_nat_le {c : cardinal} {n : ℕ} (h : cardinal.aleph_0 ≤ c) :
c ^ n ≤ c
source
theorem cardinal.power_nat_eq {c : cardinal} {n : ℕ} (h1 : cardinal.aleph_0 ≤ c) (h2 : 1 ≤ n) :
c ^ n = c
source
theorem cardinal.power_nat_le_max {c : cardinal} {n : ℕ} :
c ^ ↑n ≤ linear_order.max c cardinal.aleph_0
source
theorem cardinal.powerlt_aleph_0 {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
c ^< cardinal.aleph_0 = c
source
theorem cardinal.powerlt_aleph_0_le (c : cardinal) :
c ^< cardinal.aleph_0 ≤ linear_order.max c cardinal.aleph_0

Computing cardinality of various types #

source
@[simp]
theorem cardinal.mk_list_eq_mk (α : Type u) [infinite α] :
cardinal.mk (list α) = cardinal.mk α
source
theorem cardinal.mk_list_eq_aleph_0 (α : Type u) [countable α] [nonempty α] :
cardinal.mk (list α) = cardinal.aleph_0
source
theorem cardinal.mk_list_eq_max_mk_aleph_0 (α : Type u) [nonempty α] :
cardinal.mk (list α) = linear_order.max (cardinal.mk α) cardinal.aleph_0
source
theorem cardinal.mk_list_le_max (α : Type u) :
cardinal.mk (list α) ≤ linear_order.max cardinal.aleph_0 (cardinal.mk α)
source
@[simp]
theorem cardinal.mk_finset_of_infinite (α : Type u) [infinite α] :
cardinal.mk (finset α) = cardinal.mk α
source
@[simp]
theorem cardinal.mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [infinite α] [has_zero β] [nontrivial β] :
cardinal.mk (α →₀ β) = linear_order.max (cardinal.mk α).lift (cardinal.mk β).lift
source
theorem cardinal.mk_finsupp_of_infinite (α β : Type u) [infinite α] [has_zero β] [nontrivial β] :
cardinal.mk (α →₀ β) = linear_order.max (cardinal.mk α) (cardinal.mk β)
source
@[simp]
theorem cardinal.mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [nonempty α] [has_zero β] [infinite β] :
cardinal.mk (α →₀ β) = linear_order.max (cardinal.mk α).lift (cardinal.mk β).lift
source
theorem cardinal.mk_finsupp_of_infinite' (α β : Type u) [nonempty α] [has_zero β] [infinite β] :
cardinal.mk (α →₀ β) = linear_order.max (cardinal.mk α) (cardinal.mk β)
source
theorem cardinal.mk_finsupp_nat (α : Type u) [nonempty α] :
cardinal.mk (α →₀ ℕ) = linear_order.max (cardinal.mk α) cardinal.aleph_0
source
@[simp]
theorem cardinal.mk_multiset_of_nonempty (α : Type u) [nonempty α] :
cardinal.mk (multiset α) = linear_order.max (cardinal.mk α) cardinal.aleph_0
source
theorem cardinal.mk_multiset_of_infinite (α : Type u) [infinite α] :
cardinal.mk (multiset α) = cardinal.mk α
source
@[simp]
theorem cardinal.mk_multiset_of_is_empty (α : Type u) [is_empty α] :
cardinal.mk (multiset α) = 1
source
theorem cardinal.mk_multiset_of_countable (α : Type u) [countable α] [nonempty α] :
cardinal.mk (multiset α) = cardinal.aleph_0
source
theorem cardinal.mk_bounded_set_le_of_infinite (α : Type u) [infinite α] (c : cardinal) :
cardinal.mk {t // cardinal.mk ↥t ≤ c} ≤ cardinal.mk α ^ c
source
theorem cardinal.mk_bounded_set_le (α : Type u) (c : cardinal) :
cardinal.mk {t // cardinal.mk ↥t ≤ c} ≤ linear_order.max (cardinal.mk α) cardinal.aleph_0 ^ c
source
theorem cardinal.mk_bounded_subset_le {α : Type u} (s : set α) (c : cardinal) :
cardinal.mk {t // t ⊆ s ∧ cardinal.mk ↥t ≤ c} ≤ linear_order.max (cardinal.mk ↥s) cardinal.aleph_0 ^ c

Properties of compl #

source
theorem cardinal.mk_compl_of_infinite {α : Type u_1} [infinite α] (s : set α) (h2 : cardinal.mk ↥s < cardinal.mk α) :
cardinal.mk ↥sᶜ = cardinal.mk α
source
theorem cardinal.mk_compl_finset_of_infinite {α : Type u_1} [infinite α] (s : finset α) :
cardinal.mk ↥(↑s)ᶜ = cardinal.mk α
source
theorem cardinal.mk_compl_eq_mk_compl_infinite {α : Type u_1} [infinite α] {s t : set α} (hs : cardinal.mk ↥s < cardinal.mk α) (ht : cardinal.mk ↥t < cardinal.mk α) :
cardinal.mk ↥sᶜ = cardinal.mk ↥tᶜ
source
theorem cardinal.mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} [finite α] {s : set α} {t : set β} (h1 : (cardinal.mk α).lift = (cardinal.mk β).lift) (h2 : (cardinal.mk ↥s).lift = (cardinal.mk ↥t).lift) :
(cardinal.mk ↥sᶜ).lift = (cardinal.mk ↥tᶜ).lift
source
theorem cardinal.mk_compl_eq_mk_compl_finite {α β : Type u} [finite α] {s : set α} {t : set β} (h1 : cardinal.mk α = cardinal.mk β) (h : cardinal.mk ↥s = cardinal.mk ↥t) :
cardinal.mk ↥sᶜ = cardinal.mk ↥tᶜ
source
theorem cardinal.mk_compl_eq_mk_compl_finite_same {α : Type u_1} [finite α] {s t : set α} (h : cardinal.mk ↥s = cardinal.mk ↥t) :
cardinal.mk ↥sᶜ = cardinal.mk ↥tᶜ

Extending an injection to an equiv #

source
theorem cardinal.extend_function {α : Type u_1} {β : Type u_2} {s : set α} (f : ↥s ↪ β) (h : nonempty (↥sᶜ ≃ ↥(set.range ⇑f)ᶜ)) :
∃ (g : α ≃ β), ∀ (x : ↥s), ⇑g ↑x = ⇑f x
source
theorem cardinal.extend_function_finite {α : Type u_1} {β : Type u_2} [finite α] {s : set α} (f : ↥s ↪ β) (h : nonempty (α ≃ β)) :
∃ (g : α ≃ β), ∀ (x : ↥s), ⇑g ↑x = ⇑f x
source
theorem cardinal.extend_function_of_lt {α : Type u_1} {β : Type u_2} {s : set α} (f : ↥s ↪ β) (hs : cardinal.mk ↥s < cardinal.mk α) (h : nonempty (α ≃ β)) :
∃ (g : α ≃ β), ∀ (x : ↥s), ⇑g ↑x = ⇑f x

This section proves inequalities for bit0 and bit1, enabling simp to solve inequalities for numeral cardinals. The complexity of the resulting algorithm is not good, as in some cases simp reduces an inequality to a disjunction of two situations, depending on whether a cardinal is finite or infinite. Since the evaluation of the branches is not lazy, this is bad. It is good enough for practical situations, though.

For specific numbers, these inequalities could also be deduced from the corresponding inequalities of natural numbers using norm_cast:

example : (37 : cardinal) < 42 :=
by { norm_cast, norm_num }
source
theorem cardinal.bit0_ne_zero (a : cardinal) :
¬bit0 a = 0 ↔ ¬a = 0
source
@[simp]
theorem cardinal.bit1_ne_zero (a : cardinal) :
¬bit1 a = 0
source
@[simp]
theorem cardinal.zero_lt_bit0 (a : cardinal) :
0 < bit0 a ↔ 0 < a
source
@[simp]
theorem cardinal.zero_lt_bit1 (a : cardinal) :
0 < bit1 a
source
@[simp]
theorem cardinal.one_le_bit0 (a : cardinal) :
1 ≤ bit0 a ↔ 0 < a
source
@[simp]
theorem cardinal.one_le_bit1 (a : cardinal) :
1 ≤ bit1 a
source
theorem cardinal.bit0_eq_self {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
bit0 c = c
source
@[simp]
theorem cardinal.bit0_lt_aleph_0 {c : cardinal} :
bit0 c < cardinal.aleph_0 ↔ c < cardinal.aleph_0
source
@[simp]
theorem cardinal.aleph_0_le_bit0 {c : cardinal} :
cardinal.aleph_0 ≤ bit0 c ↔ cardinal.aleph_0 ≤ c
source
@[simp]
theorem cardinal.bit1_eq_self_iff {c : cardinal} :
bit1 c = c ↔ cardinal.aleph_0 ≤ c
source
@[simp]
theorem cardinal.bit1_lt_aleph_0 {c : cardinal} :
bit1 c < cardinal.aleph_0 ↔ c < cardinal.aleph_0
source
@[simp]
theorem cardinal.aleph_0_le_bit1 {c : cardinal} :
cardinal.aleph_0 ≤ bit1 c ↔ cardinal.aleph_0 ≤ c
source
@[simp]
theorem cardinal.bit0_le_bit0 {a b : cardinal} :
bit0 a ≤ bit0 b ↔ a ≤ b
source
@[simp]
theorem cardinal.bit0_le_bit1 {a b : cardinal} :
bit0 a ≤ bit1 b ↔ a ≤ b
source
@[simp]
theorem cardinal.bit1_le_bit1 {a b : cardinal} :
bit1 a ≤ bit1 b ↔ a ≤ b
source
@[simp]
theorem cardinal.bit1_le_bit0 {a b : cardinal} :
bit1 a ≤ bit0 b ↔ a < b ∨ a ≤ b ∧ cardinal.aleph_0 ≤ a
source
@[simp]
theorem cardinal.bit0_lt_bit0 {a b : cardinal} :
bit0 a < bit0 b ↔ a < b
source
@[simp]
theorem cardinal.bit1_lt_bit0 {a b : cardinal} :
bit1 a < bit0 b ↔ a < b
source
@[simp]
theorem cardinal.bit1_lt_bit1 {a b : cardinal} :
bit1 a < bit1 b ↔ a < b
source
@[simp]
theorem cardinal.bit0_lt_bit1 {a b : cardinal} :
bit0 a < bit1 b ↔ a < b ∨ a ≤ b ∧ a < cardinal.aleph_0
source
theorem cardinal.one_lt_two  :
1 < 2
source
@[simp]
theorem cardinal.one_lt_bit0 {a : cardinal} :
1 < bit0 a ↔ 0 < a
source
@[simp]
theorem cardinal.one_lt_bit1 (a : cardinal) :
1 < bit1 a ↔ 0 < a