# mathlibdocumentation

set_theory.cardinal

# Cardinal Numbers #

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

## Main definitions #

• cardinal the type of cardinal numbers (in a given universe).
• cardinal.mk α or #α is the cardinality of α. The notation # lives in the locale cardinal.
• There is an instance that cardinal forms a canonically_ordered_comm_semiring.
• Addition c₁ + c₂ is defined by cardinal.add_def α β : #α + #β = #(α ⊕ β).
• Multiplication c₁ * c₂ is defined by cardinal.mul_def : #α * #β = #(α * β).
• The order c₁ ≤ c₂ is defined by cardinal.le_def α β : #α ≤ #β ↔ nonempty (α ↪ β).
• Exponentiation c₁ ^ c₂ is defined by cardinal.power_def α β : #α ^ #β = #(β → α).
• cardinal.omega the cardinality of ℕ. This definition is universe polymorphic: cardinal.omega.{u} : cardinal.{u} (contrast with ℕ : Type, which lives in a specific universe). In some cases the universe level has to be given explicitly.
• cardinal.min (I : nonempty ι) (c : ι → cardinal) is the minimal cardinal in the range of c.
• cardinal.succ c is the successor cardinal, the smallest cardinal larger than c.
• cardinal.sum is the sum of a collection of cardinals.
• cardinal.sup is the supremum of a collection of cardinals.
• cardinal.powerlt c₁ c₂ or c₁ ^< c₂ is defined as sup_{γ < β} α^γ.

## Main Statements #

• Cantor's theorem: cardinal.cantor c : c < 2 ^ c.
• König's theorem: cardinal.sum_lt_prod

## Implementation notes #

• There is a type of cardinal numbers in every universe level: cardinal.{u} : Type (u + 1) is the quotient of types in Type u. The operation cardinal.lift lifts cardinal numbers to a higher level.
• Cardinal arithmetic specifically for infinite cardinals (like κ * κ = κ) is in the file set_theory/cardinal_ordinal.lean.
• There is an instance has_pow cardinal, but this will only fire if Lean already knows that both the base and the exponent live in the same universe. As a workaround, you can add
  local infixr ^ := @has_pow.pow cardinal cardinal cardinal.has_pow

to a file. This notation will work even if Lean doesn't know yet that the base and the exponent live in the same universe (but no exponents in other types can be used).

## Tags #

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

@[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
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
@[protected]
theorem cardinal.eq {α β : Type u} :
# α = # β nonempty β)
@[simp]
theorem cardinal.mk_def (α : Type u) :
α = # α
@[simp]
theorem cardinal.mk_out (c : cardinal) :
@[protected, instance]

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

Equations
theorem cardinal.le_def (α β : Type u) :
# α # β nonempty β)
theorem cardinal.mk_le_of_injective {α β : Type u} {f : α → β} (hf : function.injective 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
@[protected]
theorem cardinal.eq_congr {α β : Type u} :
α β# α = # β
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem cardinal.ne_zero_iff_nonempty {α : Type u} :
# α 0
@[protected, instance]
Equations
@[protected, instance]
theorem cardinal.le_one_iff_subsingleton {α : Type u} :
# α 1
theorem cardinal.one_lt_iff_nontrivial {α : Type u} :
1 < # α
@[protected, instance]
Equations
@[simp]
theorem cardinal.add_def (α β : Type (max u_1 u_2)) :
# α + # β = # β)
@[protected, instance]
Equations
@[simp]
theorem cardinal.mul_def (α β : Type u) :
(# α) * # β = # × β)
@[protected]
theorem cardinal.eq_zero_or_eq_zero_of_mul_eq_zero {a b : cardinal} :
a * b = 0a = 0 b = 0
@[protected, instance]
Equations
@[protected]

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

Equations
• a.power b = (λ (α β : Type u), # (β → α)) cardinal.power._proof_1
@[protected, instance]
Equations
@[simp]
theorem cardinal.power_def (α β : Type u_1) :
# α ^ # β = # (β → α)
@[simp]
theorem cardinal.power_zero {a : cardinal} :
a ^ 0 = 1
@[simp]
theorem cardinal.power_one {a : cardinal} :
a ^ 1 = a
@[simp]
theorem cardinal.one_power {a : cardinal} :
1 ^ a = 1
@[simp]
theorem cardinal.prop_eq_two  :
# (ulift Prop) = 2
@[simp]
theorem cardinal.zero_power {a : cardinal} :
a 00 ^ a = 0
theorem cardinal.power_ne_zero {a : cardinal} (b : cardinal) :
a 0a ^ b 0
theorem cardinal.mul_power {a b c : cardinal} :
(a * b) ^ c = (a ^ c) * b ^ c
theorem cardinal.power_add {a b c : cardinal} :
a ^ (b + c) = (a ^ b) * a ^ c
theorem cardinal.power_mul {a b c : cardinal} :
a ^ b * c = (a ^ b) ^ c
@[simp]
theorem cardinal.pow_cast_right (κ : cardinal) (n : ) :
κ ^ n = κ ^ n
@[protected]
theorem cardinal.zero_le (a : cardinal) :
0 a
@[protected]
a bc da + c b + d
@[protected]
b ca + b a + c
@[protected]
theorem cardinal.le_iff_exists_add {a b : cardinal} :
a b ∃ (c : cardinal), b = a + c
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem cardinal.zero_lt_one  :
0 < 1
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
@[protected, instance]
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
• f = f
theorem cardinal.min_eq {ι : Type u_1} (I : nonempty ι) (f : ι → cardinal) :
∃ (i : ι), f = f i
theorem cardinal.min_le {ι : Type u_1} {I : nonempty ι} (f : ι → cardinal) (i : ι) :
f f i
theorem cardinal.le_min {ι : Type u_1} {I : nonempty ι} {f : ι → cardinal} {a : cardinal} :
a f ∀ (i : ι), a f i
@[protected]
theorem cardinal.wf  :
@[protected, instance]
Equations
@[protected, instance]

The successor cardinal - the smallest cardinal greater than c. This is not the same as c + 1 except in the case of finite c.

Equations
theorem cardinal.lt_succ_self (c : cardinal) :
c < c.succ
theorem cardinal.succ_le {a b : cardinal} :
a.succ b a < b
theorem cardinal.lt_succ {a b : cardinal} :
a < b.succ a b
def cardinal.sum {ι : Type u_1} (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 : ι) :
f 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
• = (λ (a : {c // ∀ (i : ι), f i c}), a.val)
theorem cardinal.le_sup {ι : Type u_1} (f : ι → cardinal) (i : ι) :
f i
theorem cardinal.sup_le {ι : Type u_1} {f : ι → cardinal} {a : cardinal} :
∀ (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} (h : ι → false) :
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_ne_zero {ι : Type u_1} (f : ι → cardinal) :
∀ (i : ι), f i 0
theorem cardinal.prod_eq_zero {ι : Type u_1} (f : ι → cardinal) :
∃ (i : ι), f i = 0

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

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

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

Equations
theorem cardinal.mk_nat  :
@[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, norm_cast]
theorem cardinal.nat_cast_pow {m n : } :
(m ^ n) = m ^ n
@[simp, norm_cast]
theorem cardinal.nat_cast_le {m n : } :
m n m n
@[simp, norm_cast]
theorem cardinal.nat_cast_lt {m n : } :
m < n m < n
@[simp, norm_cast]
theorem cardinal.nat_cast_inj {m n : } :
m = n m = n
@[simp, norm_cast]
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  :
theorem cardinal.lt_omega {c : cardinal} :
∃ (n : ), c = n
theorem cardinal.omega_le {c : cardinal} :
∀ (n : ), n c
theorem cardinal.lt_omega_iff_fintype {α : Type u} :
theorem cardinal.lt_omega_iff_finite {α : Type u_1} {S : set α} :
@[protected, instance]
Equations
theorem cardinal.mul_lt_omega_iff_of_ne_zero {a b : cardinal} (ha : a 0) (hb : b 0) :
theorem cardinal.eq_one_iff_subsingleton_and_nonempty {α : Type u_1} :
# α = 1
theorem cardinal.infinite_iff {α : Type u} :
theorem cardinal.denumerable_iff {α : Type u} :
theorem cardinal.countable_iff {α : Type u} (s : set α) :

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

Equations
@[simp]
@[simp]
theorem cardinal.to_nat_cast (n : ) :

to_nat has a right-inverse: coercion.

@[simp]
theorem cardinal.mk_to_nat_of_infinite {α : Type u} [h : infinite α] :
= 0
@[simp]
theorem cardinal.mk_to_nat_eq_card {α : Type u} [fintype α] :
@[simp]
theorem cardinal.zero_to_nat  :
@[simp]
theorem cardinal.one_to_nat  :

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

Equations
@[simp]
theorem cardinal.to_enat_cast (n : ) :
@[simp]
theorem cardinal.mk_to_enat_of_infinite {α : Type u} [h : infinite α] :
@[simp]
theorem cardinal.mk_to_enat_eq_coe_card {α : Type u} [fintype α] :
theorem cardinal.mk_int  :
theorem cardinal.mk_pnat  :
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  :
= 0
@[simp]
theorem cardinal.mk_pempty  :
= 0
@[simp]
theorem cardinal.mk_plift_of_false {p : Prop} (h : ¬p) :
# (plift p) = 0
theorem cardinal.mk_unit  :
= 1
@[simp]
theorem cardinal.mk_punit  :
= 1
@[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_bool  :
= 2
@[simp]
theorem cardinal.mk_Prop  :
# Prop = 2
@[simp]
theorem cardinal.mk_set {α : Type u} :
# (set α) = 2 ^ # α
@[simp]
theorem cardinal.mk_option {α : Type u} :
# (option α) = # α + 1
theorem cardinal.mk_list_eq_sum_pow (α : Type u) :
# (list α) = cardinal.sum (λ (n : ), # α ^ n)
theorem cardinal.mk_quot_le {α : Type u} {r : α → α → Prop} :
# (quot r) # α
theorem cardinal.mk_quotient_le {α : Type u} {s : setoid α} :
# (quotient s) # α
theorem cardinal.mk_subtype_le {α : Type u} (p : α → Prop) :
# (subtype p) # α
theorem cardinal.mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x : α⦄, p xq x) :
@[simp]
theorem cardinal.mk_emptyc (α : Type u) :
= 0
theorem cardinal.mk_emptyc_iff {α : Type u} {s : set α} :
# s = 0 s =
theorem cardinal.mk_univ {α : Type u} :
= # α
theorem cardinal.mk_image_le {α β : Type u} {f : α → β} {s : set α} :
# (f '' s) # s
theorem cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(# (f '' s)).lift (# s).lift
theorem cardinal.mk_range_le {α β : Type u} {f : α → β} :
theorem cardinal.mk_range_eq {α β : Type u} (f : α → β) (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 α} :
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 : T) :
# (S T) = # S + # T
theorem cardinal.mk_sum_compl {α : Type u_1} (s : set α) :
# s + # s = # α
theorem cardinal.mk_le_mk_of_subset {α : Type u_1} {s t : set α} (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_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 : s) :
(# (f '' s)).lift = (# s).lift
theorem cardinal.mk_image_eq_of_inj_on {α β : Type u} (f : α → β) (s : set α) (h : 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 ) :
(# 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 ) :
(# (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 ) :
theorem cardinal.mk_preimage_of_injective_of_subset_range {α β : Type u} (f : α → β) (s : set β) (h : function.injective f) (h2 : s ) :
# (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 // mk 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
theorem equiv.cardinal_eq {α β : Type u_1} :
α β# α = # β