mathlib documentation

set_theory.cardinal.basic

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

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, instance]
def cardinal.can_lift_cardinal_Type  :
can_lift cardinal (Type u)
Equations
source
theorem cardinal.induction_on {p : cardinal → Prop} (c : cardinal) (h : ∀ (α : Type u_1), p (# α)) :
p c
source
theorem cardinal.induction_on₂ {p : cardinal → cardinal → Prop} (c₁ : cardinal) (c₂ : cardinal) (h : ∀ (α : Type u_1) (β : Type u_2), p (# α) (# β)) :
p c₁ c₂
source
theorem cardinal.induction_on₃ {p : cardinal → cardinal → cardinal → Prop} (c₁ : cardinal) (c₂ : cardinal) (c₃ : cardinal) (h : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), p (# α) (# β) (# γ)) :
p c₁ c₂ c₃
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
noncomputable def cardinal.out_mk_equiv {α : Type v} :
quotient.out (# α) ≃ α

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

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

Alias of mk_congr.

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

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

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

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

Equations
source
def cardinal.lift (c : cardinal) :
cardinal

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

Equations
source
@[simp]
theorem cardinal.mk_ulift (α : Type u) :
# (ulift α) = (# α).lift
source
theorem cardinal.lift_umax  :
cardinal.lift = cardinal.lift
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_uzero (a : cardinal) :
a.lift = a
source
@[simp]
theorem cardinal.lift_lift (a : cardinal) :
a.lift.lift = a.lift
source
@[protected, instance]
def cardinal.has_le  :
has_le cardinal

We define the order on cardinal numbers by #α ≤ #β 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 function.embedding.cardinal_le {α β : Type u} (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.mk_subtype_le {α : Type u} (p : α → Prop) :
# (subtype p) ≤ # α
source
theorem cardinal.mk_set_le {α : Type u} (s : set α) :
# ↥s ≤ # α
source
theorem cardinal.out_embedding {c c' : cardinal} :
c ≤ c' ↔ nonempty (quotient.out c ↪ quotient.out c')
source
@[protected, instance]
def cardinal.preorder  :
preorder cardinal
Equations
source
@[protected, instance]
def cardinal.partial_order  :
partial_order cardinal
Equations
source
theorem cardinal.lift_mk_le {α : Type u} {β : Type v} :
(# α).lift ≤ (# β).lift ↔ nonempty (α ↪ β)
source
theorem cardinal.lift_mk_le' {α : Type u} {β : Type v} :
(# α).lift ≤ (# β).lift ↔ nonempty (α ↪ β)

A variant of cardinal.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.

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

A variant of cardinal.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.

source
@[simp]
theorem cardinal.lift_le {a b : cardinal} :
a.lift ≤ b.lift ↔ a ≤ b
source
def cardinal.lift_order_embedding  :
cardinal ↪o cardinal

cardinal.lift as an order_embedding.

Equations
source
@[simp]
theorem cardinal.lift_order_embedding_apply  :
⇑cardinal.lift_order_embedding = cardinal.lift
source
theorem cardinal.lift_injective  :
function.injective cardinal.lift
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
@[protected, instance]
def cardinal.has_zero  :
has_zero cardinal
Equations
source
@[protected, instance]
def cardinal.inhabited  :
inhabited cardinal
Equations
source
theorem cardinal.mk_eq_zero (α : Type u) [is_empty α] :
# α = 0
source
@[simp]
theorem cardinal.lift_zero  :
0.lift = 0
source
@[simp]
theorem cardinal.lift_eq_zero {a : cardinal} :
a.lift = 0 ↔ a = 0
source
theorem cardinal.mk_eq_zero_iff {α : Type u} :
# α = 0 ↔ is_empty α
source
theorem cardinal.mk_ne_zero_iff {α : Type u} :
# α ≠ 0 ↔ nonempty α
source
@[simp]
theorem cardinal.mk_ne_zero (α : Type u) [nonempty α] :
# α ≠ 0
source
@[protected, instance]
def cardinal.has_one  :
has_one cardinal
Equations
source
@[protected, instance]
def cardinal.nontrivial  :
nontrivial cardinal
source
theorem cardinal.mk_eq_one (α : Type u) [unique α] :
# α = 1
source
theorem cardinal.le_one_iff_subsingleton {α : Type u} :
# α ≤ 1 ↔ subsingleton α
source
@[protected, instance]
def cardinal.has_add  :
has_add cardinal
Equations
source
theorem cardinal.add_def (α β : Type u) :
# α + # β = # (α ⊕ β)
source
@[simp]
theorem cardinal.mk_sum (α : Type u) (β : Type v) :
# (α ⊕ β) = (# α).lift + (# β).lift
source
@[simp]
theorem cardinal.mk_option {α : Type u} :
# (option α) = # α + 1
source
@[simp]
theorem cardinal.mk_psum (α : Type u) (β : Type v) :
# (psum α β) = (# α).lift + (# β).lift
source
@[simp]
theorem cardinal.mk_fintype (α : Type u) [fintype α] :
# α = ↑(fintype.card α)
source
@[protected, instance]
def cardinal.has_mul  :
has_mul cardinal
Equations
source
theorem cardinal.mul_def (α β : Type u) :
(# α) * # β = # (α × β)
source
@[simp]
theorem cardinal.mk_prod (α : Type u) (β : Type v) :
# (α × β) = ((# α).lift) * (# β).lift
source
@[protected]
theorem cardinal.add_comm (a b : cardinal) :
a + b = b + a
source
@[protected]
theorem cardinal.mul_comm (a b : cardinal) :
a * b = b * a
source
@[protected]
theorem cardinal.zero_add (a : cardinal) :
0 + a = a
source
@[protected]
theorem cardinal.zero_mul (a : cardinal) :
0 * a = 0
source
@[protected]
theorem cardinal.one_mul (a : cardinal) :
1 * a = a
source
@[protected]
theorem cardinal.left_distrib (a b c : cardinal) :
a * (b + c) = a * b + a * c
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]
def cardinal.power (a b : cardinal) :
cardinal

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

Equations
source
@[protected, instance]
def cardinal.has_pow  :
has_pow cardinal cardinal
Equations
source
theorem cardinal.power_def (α β : Type u_1) :
# α ^ # β = # (β → α)
source
theorem cardinal.mk_arrow (α : Type u) (β : Type v) :
# (α → β) = (# β).lift ^ (# α).lift
source
@[simp]
theorem cardinal.lift_power (a b : cardinal) :
(a ^ b).lift = a.lift ^ b.lift
source
@[simp]
theorem cardinal.power_zero {a : cardinal} :
a ^ 0 = 1
source
@[simp]
theorem cardinal.power_one {a : cardinal} :
a ^ 1 = a
source
theorem cardinal.power_add {a b c : cardinal} :
a ^ (b + c) = (a ^ b) * a ^ c
source
@[protected, instance]
def cardinal.comm_semiring  :
comm_semiring cardinal
Equations
source
theorem cardinal.power_bit0 (a b : cardinal) :
a ^ bit0 b = (a ^ b) * a ^ b
source
theorem cardinal.power_bit1 (a b : cardinal) :
a ^ bit1 b = ((a ^ b) * a ^ b) * a
source
@[simp]
theorem cardinal.one_power {a : cardinal} :
1 ^ a = 1
source
@[simp]
theorem cardinal.mk_bool  :
# bool = 2
source
@[simp]
theorem cardinal.mk_Prop  :
# 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_mul {a b c : cardinal} :
a ^ b * c = (a ^ b) ^ c
source
@[simp]
theorem cardinal.pow_cast_right (κ : cardinal) (n : ℕ) :
κ ^ ↑n = κ ^ n
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_bit0 (a : cardinal) :
(bit0 a).lift = bit0 a.lift
source
@[simp]
theorem cardinal.lift_bit1 (a : cardinal) :
(bit1 a).lift = bit1 a.lift
source
theorem cardinal.lift_two  :
2.lift = 2
source
@[simp]
theorem cardinal.mk_set {α : Type u} :
# (set α) = 2 ^ # α
source
theorem cardinal.lift_two_power (a : cardinal) :
(2 ^ a).lift = 2 ^ a.lift
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
@[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.self_le_power (a : cardinal) {b : cardinal} (hb : 1 ≤ b) :
a ≤ a ^ b
source
theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a

Cantor's theorem

source
@[protected, instance]
def cardinal.no_max_order  :
no_max_order cardinal
source
@[protected, instance]
noncomputable def cardinal.linear_order  :
linear_order cardinal
Equations
source
@[protected, instance]
noncomputable def cardinal.canonically_linear_ordered_add_monoid  :
canonically_linear_ordered_add_monoid cardinal
Equations
source
@[protected, instance]
noncomputable def cardinal.distrib_lattice  :
distrib_lattice cardinal
Equations
source
theorem cardinal.one_lt_iff_nontrivial {α : Type u} :
1 < # α ↔ nontrivial α
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
@[protected]
noncomputable 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 min_injective).

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]
noncomputable def cardinal.conditionally_complete_linear_order_bot  :
conditionally_complete_linear_order_bot cardinal
Equations
source
@[protected, instance]
def cardinal.wo  :
is_well_order cardinal has_lt.lt
source
noncomputable 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.succ_nonempty (c : cardinal) :
{c' : cardinal | c < c'}.nonempty
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
@[simp]
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_pos (c : cardinal) :
0 < 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.mk_sigma {ι : Type u_1} (f : ι → Type u_2) :
# (Σ (i : ι), f i) = cardinal.sum (λ (i : ι), # (f i))
source
@[simp]
theorem cardinal.sum_const (ι : Type u) (a : cardinal) :
cardinal.sum (λ (i : ι), a) = ((# ι).lift) * a.lift
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
theorem cardinal.mk_le_mk_mul_of_mk_preimage_le {α β : Type u} {c : cardinal} (f : α → β) (hf : ∀ (b : β), # ↥(f ⁻¹' {b}) ≤ c) :
# α ≤ (# β) * c
source
theorem cardinal.bdd_above_range {ι : Type u} (f : ι → cardinal) :
bdd_above (set.range f)

The range of an indexed cardinal function, whose outputs live in a higher universe than the inputs, is always bounded above.

source
@[protected, instance]
def cardinal.set.Iic.small (a : cardinal) :
small ↥(set.Iic a)
source
theorem cardinal.bdd_above_iff_small (s : set cardinal) :
bdd_above s ↔ small ↥s

A set of cardinals is bounded above iff it's small, i.e. it corresponds to an usual ZFC set.

source
noncomputable def cardinal.sup {ι : Type u} (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} (f : ι → cardinal) (i : ι) :
f i ≤ cardinal.sup f
source
theorem cardinal.sup_le_iff {ι : Type u_1} {f : ι → cardinal} {a : cardinal} :
cardinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
source
theorem cardinal.sup_le {ι : Type u_1} {f : ι → cardinal} {a : cardinal} :
(∀ (i : ι), f i ≤ a) → cardinal.sup f ≤ 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.sum_le_sup_lift {ι : Type u} (f : ι → cardinal) :
cardinal.sum f ≤ ((# ι).lift) * cardinal.sup f
source
theorem cardinal.sup_eq_zero {ι : Type u_1} {f : ι → cardinal} [is_empty ι] :
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.mk_pi {ι : Type u} (α : ι → Type v) :
# (Π (i : ι), α i) = cardinal.prod (λ (i : ι), # (α i))
source
@[simp]
theorem cardinal.prod_const (ι : Type u) (a : cardinal) :
cardinal.prod (λ (i : ι), a) = a.lift ^ (# ι).lift
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
@[simp]
theorem cardinal.prod_eq_zero {ι : Type u_1} (f : ι → cardinal) :
cardinal.prod f = 0 ↔ ∃ (i : ι), f i = 0
source
theorem cardinal.prod_ne_zero {ι : Type u_1} (f : ι → cardinal) :
cardinal.prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
source
@[simp]
theorem cardinal.lift_prod {ι : Type u} (c : ι → cardinal) :
(cardinal.prod c).lift = cardinal.prod (λ (i : ι), (c i).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
@[simp]
theorem cardinal.lift_min' {a b : cardinal} :
(min a b).lift = min a.lift b.lift
source
@[simp]
theorem cardinal.lift_max' {a b : cardinal} :
(max a b).lift = max a.lift b.lift
source
@[protected]
theorem cardinal.le_sup_iff {ι : Type v} {f : ι → cardinal} {c : cardinal} :
c ≤ cardinal.sup f ↔ ∀ (b : cardinal), (∀ (i : ι), f i ≤ b) → c ≤ b
source
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.

source
theorem cardinal.lift_sup_le {ι : Type v} (f : ι → cardinal) (t : cardinal) (w : ∀ (i : ι), (f i).lift ≤ t) :
(cardinal.sup f).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.

source
@[simp]
theorem cardinal.lift_sup_le_iff {ι : Type v} (f : ι → cardinal) (t : cardinal) :
(cardinal.sup f).lift ≤ t ↔ ∀ (i : ι), (f i).lift ≤ t
source
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) :
(cardinal.sup f).lift ≤ (cardinal.sup f').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.

source
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) :
(cardinal.sup f).lift ≤ (cardinal.sup f').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.

source
def cardinal.omega  :
cardinal

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

Equations
source
theorem cardinal.mk_nat  :
# ℕ = ω
source
theorem cardinal.omega_ne_zero  :
ω ≠ 0
source
theorem cardinal.omega_pos  :
0 < ω
source
@[simp]
theorem cardinal.lift_omega  :
ω.lift = ω
source
@[simp]
theorem cardinal.omega_le_lift {c : cardinal} :
ω ≤ c.lift ↔ ω ≤ c
source
@[simp]
theorem cardinal.lift_le_omega {c : cardinal} :
c.lift ≤ ω ↔ c ≤ ω

Properties about the cast from ℕ #

source
@[simp]
theorem cardinal.mk_fin (n : ℕ) :
# (fin n) = ↑n
source
@[simp]
theorem cardinal.lift_nat_cast (n : ℕ) :
↑n.lift = ↑n
source
@[simp]
theorem cardinal.lift_eq_nat_iff {a : cardinal} {n : ℕ} :
a.lift = ↑n ↔ a = ↑n
source
@[simp]
theorem cardinal.nat_eq_lift_iff {n : ℕ} {a : cardinal} :
↑n = a.lift ↔ ↑n = a
source
theorem cardinal.lift_mk_fin (n : ℕ) :
(# (fin n)).lift = ↑n
source
theorem cardinal.mk_finset {α : Type u} {s : finset α} :
# ↥s = ↑(s.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
@[protected, instance]
def cardinal.char_zero  :
char_zero cardinal
source
theorem cardinal.nat_cast_inj {m n : ℕ} :
↑m = ↑n ↔ m = n
source
theorem cardinal.nat_cast_injective  :
function.injective coe
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 < ω
source
@[simp]
theorem cardinal.one_lt_omega  :
1 < ω
source
theorem cardinal.lt_omega {c : cardinal} :
c < ω ↔ ∃ (n : ℕ), c = ↑n
source
theorem cardinal.omega_le {c : cardinal} :
ω ≤ c ↔ ∀ (n : ℕ), ↑n ≤ c
source
theorem cardinal.lt_omega_iff_fintype {α : Type u} :
# α < ω ↔ nonempty (fintype α)
source
theorem cardinal.lt_omega_of_fintype (α : Type u) [fintype α] :
# α < ω
source
theorem cardinal.lt_omega_iff_finite {α : Type u_1} {S : set α} :
# ↥S < ω ↔ 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 < ω) (hb : b < ω) :
a + b < ω
source
theorem cardinal.add_lt_omega_iff {a b : cardinal} :
a + b < ω ↔ a < ω ∧ b < ω
source
theorem cardinal.omega_le_add_iff {a b : cardinal} :
ω ≤ a + b ↔ ω ≤ a ∨ ω ≤ b
source
theorem cardinal.mul_lt_omega {a b : cardinal} (ha : a < ω) (hb : b < ω) :
a * b < ω
source
theorem cardinal.mul_lt_omega_iff {a b : cardinal} :
a * b < ω ↔ a = 0 ∨ b = 0 ∨ a < ω ∧ b < ω
source
theorem cardinal.omega_le_mul_iff {a b : cardinal} :
ω ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ω ≤ a ∨ ω ≤ b)
source
theorem cardinal.mul_lt_omega_iff_of_ne_zero {a b : cardinal} (ha : a ≠ 0) (hb : b ≠ 0) :
a * b < ω ↔ a < ω ∧ b < ω
source
theorem cardinal.power_lt_omega {a b : cardinal} (ha : a < ω) (hb : b < ω) :
a ^ b < ω
source
theorem cardinal.eq_one_iff_unique {α : Type u_1} :
# α = 1 ↔ subsingleton α ∧ nonempty α
source
theorem cardinal.infinite_iff {α : Type u} :
infinite α ↔ ω ≤ # α
source
@[simp]
theorem cardinal.omega_le_mk (α : Type u) [infinite α] :
ω ≤ # α
source
theorem cardinal.encodable_iff {α : Type u} :
nonempty (encodable α) ↔ # α ≤ ω
source
@[simp]
theorem cardinal.mk_le_omega {α : Type u} [encodable α] :
# α ≤ ω
source
theorem cardinal.denumerable_iff {α : Type u} :
nonempty (denumerable α) ↔ # α = ω
source
@[simp]
theorem cardinal.mk_denumerable (α : Type u) [denumerable α] :
# α = ω
source
@[simp]
theorem cardinal.mk_set_le_omega {α : Type u} (s : set α) :
# ↥s ≤ ω ↔ s.countable
source
@[simp]
theorem cardinal.omega_add_omega  :
ω + ω = ω
source
theorem cardinal.omega_mul_omega  :
ω * ω = ω
source
@[simp]
theorem cardinal.add_le_omega {c₁ c₂ : cardinal} :
c₁ + c₂ ≤ ω ↔ c₁ ≤ ω ∧ c₂ ≤ ω
source
noncomputable 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.to_nat c = classical.some _
source
@[simp]
theorem cardinal.to_nat_apply_of_omega_le {c : cardinal} (h : ω ≤ c) :
⇑cardinal.to_nat c = 0
source
@[simp]
theorem cardinal.cast_to_nat_of_lt_omega {c : cardinal} (h : c < ω) :
↑(⇑cardinal.to_nat c) = c
source
@[simp]
theorem cardinal.cast_to_nat_of_omega_le {c : cardinal} (h : ω ≤ c) :
↑(⇑cardinal.to_nat c) = 0
source
theorem cardinal.to_nat_le_iff_le_of_lt_omega {c d : cardinal} (hc : c < ω) (hd : d < ω) :
⇑cardinal.to_nat c ≤ ⇑cardinal.to_nat d ↔ c ≤ d
source
theorem cardinal.to_nat_lt_iff_lt_of_lt_omega {c d : cardinal} (hc : c < ω) (hd : d < ω) :
⇑cardinal.to_nat c < ⇑cardinal.to_nat d ↔ c < d
source
theorem cardinal.to_nat_le_of_le_of_lt_omega {c d : cardinal} (hd : d < ω) (hcd : c ≤ d) :
⇑cardinal.to_nat c ≤ ⇑cardinal.to_nat d
source
theorem cardinal.to_nat_lt_of_lt_of_lt_omega {c d : cardinal} (hd : d < ω) (hcd : c < d) :
⇑cardinal.to_nat c < ⇑cardinal.to_nat d
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
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
@[simp]
theorem cardinal.to_nat_eq_one {c : cardinal} :
⇑cardinal.to_nat c = 1 ↔ c = 1
source
theorem cardinal.to_nat_eq_one_iff_unique {α : Type u_1} :
⇑cardinal.to_nat (# α) = 1 ↔ subsingleton α ∧ nonempty α
source
@[simp]
theorem cardinal.to_nat_lift (c : cardinal) :
⇑cardinal.to_nat c.lift = ⇑cardinal.to_nat c
source
theorem cardinal.to_nat_congr {α : Type u} {β : Type v} (e : α ≃ β) :
⇑cardinal.to_nat (# α) = ⇑cardinal.to_nat (# β)
source
@[simp]
theorem cardinal.to_nat_mul (x y : cardinal) :
⇑cardinal.to_nat (x * y) = (⇑cardinal.to_nat x) * ⇑cardinal.to_nat y
source
@[simp]
theorem cardinal.to_nat_add_of_lt_omega {a : cardinal} {b : cardinal} (ha : a < ω) (hb : b < ω) :
⇑cardinal.to_nat (a.lift + b.lift) = ⇑cardinal.to_nat a + ⇑cardinal.to_nat b
source
noncomputable 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.to_enat c = ↑(⇑cardinal.to_nat c)
source
@[simp]
theorem cardinal.to_enat_apply_of_omega_le {c : cardinal} (h : ω ≤ 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
theorem cardinal.mk_to_enat_eq_coe_card {α : Type u} [fintype α] :
⇑cardinal.to_enat (# α) = ↑(fintype.card α)
source
theorem cardinal.mk_int  :
# ℤ = ω
source
theorem cardinal.mk_pnat  :
# ℕ+ = ω
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_punit  :
# punit = 1
source
theorem cardinal.mk_unit  :
# unit = 1
source
@[simp]
theorem cardinal.mk_singleton {α : Type u} (x : α) :
# ↥{x} = 1
source
@[simp]
theorem cardinal.mk_plift_true  :
# (plift true) = 1
source
@[simp]
theorem cardinal.mk_plift_false  :
# (plift false) = 0
source
@[simp]
theorem cardinal.mk_vector (α : Type u) (n : ℕ) :
# (vector α n) = # α ^ n
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_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
@[simp]
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_le_lift {α : Type u} {β : Type v} {f : α → β} :
(# ↥(set.range f)).lift ≤ (# α).lift
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
theorem cardinal.finset_card_lt_omega {α : Type u} (s : finset α) :
# ↥↑s < ω
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_insert {α : Type u} {s : set α} {a : α} (h : a ∉ s) :
# ↥(insert a s) = # ↥s + 1
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_union_le_omega {α : Type u_1} {P Q : set α} :
# ↥(P ∪ Q) ≤ ω ↔ # ↥P ≤ ω ∧ # ↥Q ≤ ω
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
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.exists_not_mem_of_length_le {α : Type u_1} (l : list α) (h : ↑(l.length) < # α) :
∃ (z : α), z ∉ l
source
theorem cardinal.three_le {α : Type u_1} (h : 3 ≤ # α) (x y : α) :
∃ (z : α), z ≠ x ∧ z ≠ y
source
noncomputable def cardinal.powerlt (α β : cardinal) :
cardinal

The function α^{<β}, defined to be sup_{γ < β} α^γ. We index over {s : set β.out // #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