mathlib3documentation

set_theory.cardinal.basic

Cardinal Numbers #

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

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`.
• 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.is_limit c` means that `c` is a (weak) limit cardinal: `c ≠ 0 ∧ ∀ x < c, succ x < c`.
• `cardinal.aleph_0` or `ℵ₀` is the cardinality of `ℕ`. This definition is universe polymorphic: `cardinal.aleph_0.{u} : cardinal.{u}` (contrast with `ℕ : Type`, which lives in a specific universe). In some cases the universe level has to be given explicitly.
• `cardinal.sum` is the sum of an indexed family of cardinals, i.e. the cardinality of the corresponding sigma type.
• `cardinal.prod` is the product of an indexed family of cardinals, i.e. the cardinality of the corresponding pi type.
• `cardinal.powerlt a b` or `a ^< b` is defined as the supremum of `a ^ c` for `c < b`.

Main instances #

• Cardinals form a `canonically_ordered_comm_semiring` with the aforementioned sum and product.
• Cardinals form a `succ_order`. Use `order.succ c` for the smallest cardinal greater than `c`.
• The less than relation on cardinals forms a well-order.
• Cardinals form a `conditionally_complete_linear_order_bot`. Bounded sets for cardinals in universe `u` are precisely the sets indexed by some type in universe `u`, see `cardinal.bdd_above_iff_small`. One can use `Sup` for the cardinal supremum, and `Inf` for the minimum of a set of cardinals.

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 (name := cardinal.pow) ^ := @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, aleph, Cantor's theorem, König's theorem, Konig's theorem

@[protected, instance]

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
Instances for `cardinal`
def cardinal.mk  :

The cardinal number of a type

Equations
Instances for `cardinal.mk`
@[protected, instance]
Equations
theorem cardinal.induction_on {p : cardinal Prop} (c : cardinal) (h : (α : Type u_1), p (cardinal.mk α)) :
p c
theorem cardinal.induction_on₂ {p : cardinal cardinal Prop} (c₁ : cardinal) (c₂ : cardinal) (h : (α : Type u_1) (β : Type u_2), p (cardinal.mk α) (cardinal.mk β)) :
p c₁ c₂
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 (cardinal.mk α) (cardinal.mk β) (cardinal.mk γ)) :
p c₁ c₂ c₃
@[protected]
theorem cardinal.eq {α β : Type u} :
nonempty β)
@[simp]
theorem cardinal.mk_def (α : Type u) :
@[simp]
theorem cardinal.mk_out (c : cardinal) :
= c
noncomputable def cardinal.out_mk_equiv {α : Type v} :
α

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

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

Alias of `cardinal.mk_congr`.

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

Lift a function between `Type*`s to a function between `cardinal`s.

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

Lift a binary operation `Type* → Type* → Type*` to a binary operation on `cardinal`s.

Equations
• hf =

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

Equations
@[simp]
theorem cardinal.mk_ulift (α : Type u) :
@[simp]

`lift.{(max u v) u}` equals `lift.{v u}`. Using `set_option pp.universes true` will make it much easier to understand what's happening when using this lemma.

@[simp]

`lift.{(max v u) u}` equals `lift.{v u}`. Using `set_option pp.universes true` will make it much easier to understand what's happening when using this lemma.

@[simp]
theorem cardinal.lift_id' (a : cardinal) :
a.lift = a

A cardinal lifted to a lower or equal universe equals itself.

@[simp]
theorem cardinal.lift_id (a : cardinal) :
a.lift = a

A cardinal lifted to the same universe equals itself.

@[simp]
theorem cardinal.lift_uzero (a : cardinal) :
a.lift = a

A cardinal lifted to the zero universe equals itself.

@[simp]
theorem cardinal.lift_lift (a : cardinal) :
@[protected, instance]

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

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def cardinal.linear_order  :
Equations
theorem cardinal.le_def (α β : Type u) :
nonempty β)
theorem cardinal.mk_le_of_injective {α β : Type u} {f : α β} (hf : function.injective f) :
theorem function.embedding.cardinal_le {α β : Type u} (f : α β) :
theorem cardinal.mk_le_of_surjective {α β : Type u} {f : α β} (hf : function.surjective f) :
theorem cardinal.le_mk_iff_exists_set {c : cardinal} {α : Type u} :
c (p : set α),
theorem cardinal.mk_subtype_le {α : Type u} (p : α Prop) :
theorem cardinal.mk_set_le {α : Type u} (s : set α) :
theorem cardinal.lift_mk_le {α : Type u} {β : Type v} :
theorem cardinal.lift_mk_le' {α : Type u} {β : Type v} :

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.

theorem cardinal.lift_mk_eq {α : Type u} {β : Type v} :
theorem cardinal.lift_mk_eq' {α : Type u} {β : Type v} :

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.

@[simp]
theorem cardinal.lift_le {a b : cardinal} :
a.lift b.lift a b

`cardinal.lift` as an `order_embedding`.

Equations
@[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
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem cardinal.mk_eq_zero (α : Type u) [is_empty α] :
= 0
@[simp]
theorem cardinal.lift_zero  :
0.lift = 0
@[simp]
theorem cardinal.lift_eq_zero {a : cardinal} :
a.lift = 0 a = 0
theorem cardinal.mk_eq_zero_iff {α : Type u} :
= 0
theorem cardinal.mk_ne_zero_iff {α : Type u} :
0
@[simp]
theorem cardinal.mk_ne_zero (α : Type u) [nonempty α] :
0
@[protected, instance]
Equations
@[protected, instance]
theorem cardinal.mk_eq_one (α : Type u) [unique α] :
= 1
@[simp]

Alias of the reverse direction of `cardinal.mk_le_one_iff_set_subsingleton`.

@[protected, instance]
Equations
theorem cardinal.add_def (α β : Type u) :
= cardinal.mk β)
@[protected, instance]
Equations
@[simp]
theorem cardinal.mk_sum (α : Type u) (β : Type v) :
@[simp]
theorem cardinal.mk_option {α : Type u} :
= + 1
@[simp]
theorem cardinal.mk_psum (α : Type u) (β : Type v) :
@[simp]
theorem cardinal.mk_fintype (α : Type u) [fintype α] :
@[protected, instance]
Equations
theorem cardinal.mul_def (α β : Type u) :
= cardinal.mk × β)
@[simp]
theorem cardinal.mk_prod (α : Type u) (β : Type v) :
@[protected, instance]

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

Equations
theorem cardinal.power_def (α β : Type u_1) :
= cardinal.mk α)
theorem cardinal.mk_arrow (α : Type u) (β : Type v) :
@[simp]
theorem cardinal.lift_power (a b : cardinal) :
(a ^ b).lift = a.lift ^ b.lift
@[simp]
theorem cardinal.power_zero {a : cardinal} :
a ^ 0 = 1
@[simp]
theorem cardinal.power_one {a : cardinal} :
a ^ 1 = a
theorem cardinal.power_add {a b c : cardinal} :
a ^ (b + c) = a ^ b * a ^ c
@[protected, instance]
Equations
theorem cardinal.power_bit0 (a b : cardinal) :
a ^ bit0 b = a ^ b * a ^ b
theorem cardinal.power_bit1 (a b : cardinal) :
a ^ bit1 b = a ^ b * a ^ b * a
@[simp]
theorem cardinal.one_power {a : cardinal} :
1 ^ a = 1
@[simp]
theorem cardinal.mk_bool  :
@[simp]
theorem cardinal.mk_Prop  :
cardinal.mk Prop = 2
@[simp]
theorem cardinal.zero_power {a : cardinal} :
a 0 0 ^ a = 0
theorem cardinal.power_ne_zero {a : cardinal} (b : cardinal) :
a 0 a ^ b 0
theorem cardinal.mul_power {a b c : cardinal} :
(a * b) ^ c = a ^ c * b ^ c
theorem cardinal.power_mul {a b c : cardinal} :
a ^ (b * c) = (a ^ b) ^ c
@[simp]
theorem cardinal.pow_cast_right (a : cardinal) (n : ) :
a ^ n = a ^ n
@[simp]
theorem cardinal.lift_one  :
1.lift = 1
@[simp]
theorem cardinal.lift_add (a b : cardinal) :
(a + b).lift = a.lift + b.lift
@[simp]
theorem cardinal.lift_mul (a b : cardinal) :
(a * b).lift = a.lift * b.lift
@[simp]
theorem cardinal.lift_bit0 (a : cardinal) :
@[simp]
theorem cardinal.lift_bit1 (a : cardinal) :
theorem cardinal.lift_two  :
2.lift = 2
@[simp]
theorem cardinal.mk_set {α : Type u} :
cardinal.mk (set α) = 2 ^
@[simp]
theorem cardinal.mk_powerset {α : Type u} (s : set α) :
=

A variant of `cardinal.mk_set` expressed in terms of a `set` instead of a `Type`.

theorem cardinal.lift_two_power (a : cardinal) :
(2 ^ a).lift = 2 ^ a.lift
@[protected]
theorem cardinal.zero_le (a : cardinal) :
0 a
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem cardinal.zero_power_le (c : cardinal) :
0 ^ c 1
theorem cardinal.power_le_power_left {a b c : cardinal} :
a 0 b c a ^ b a ^ c
theorem cardinal.self_le_power (a : cardinal) {b : cardinal} (hb : 1 b) :
a a ^ b
theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a

Cantor's theorem

@[protected, instance]
@[protected, instance]
noncomputable def cardinal.distrib_lattice  :
Equations
theorem cardinal.power_le_max_power_one {a b c : cardinal} (h : b c) :
a ^ b linear_order.max (a ^ c) 1
theorem cardinal.power_le_power_right {a b c : cardinal} :
a b a ^ c b ^ c
theorem cardinal.power_pos {a : cardinal} (b : cardinal) (ha : 0 < a) :
0 < a ^ b
@[protected]
theorem cardinal.lt_wf  :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem cardinal.Inf_empty  :
@[protected, instance]
noncomputable def cardinal.succ_order  :

Note that the successor of `c` is not the same as `c + 1` except in the case of finite `c`.

Equations
theorem cardinal.succ_def (c : cardinal) :
= has_Inf.Inf {c' : cardinal | c < c'}
theorem cardinal.succ_pos (c : cardinal) :
0 <
def cardinal.is_limit (c : cardinal) :
Prop

A cardinal is a limit if it is not zero or a successor cardinal. Note that `ℵ₀` is a limit cardinal by this definition, but `0` isn't.

Use `is_succ_limit` if you want to include the `c = 0` case.

Equations
@[protected]
theorem cardinal.is_limit.ne_zero {c : cardinal} (h : c.is_limit) :
c 0
@[protected]
theorem cardinal.is_limit.succ_lt {x c : cardinal} (h : c.is_limit) :
x < c < c
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.mk_sigma {ι : Type u_1} (f : ι Type u_2) :
cardinal.mk (Σ (i : ι), f i) = cardinal.sum (λ (i : ι), cardinal.mk (f i))
@[simp]
theorem cardinal.sum_const (ι : Type u) (a : cardinal) :
cardinal.sum (λ (i : ι), a) = (cardinal.mk ι).lift * a.lift
theorem cardinal.sum_const' (ι : Type u) (a : cardinal) :
cardinal.sum (λ (_x : ι), a) = * a
@[simp]
theorem cardinal.sum_add_distrib {ι : Type u_1} (f g : ι cardinal) :
@[simp]
theorem cardinal.sum_add_distrib' {ι : Type u_1} (f g : ι cardinal) :
cardinal.sum (λ (i : ι), f i + g i) =
@[simp]
theorem cardinal.lift_sum {ι : Type u} (f : ι cardinal) :
(cardinal.sum f).lift = cardinal.sum (λ (i : ι), (f i).lift)
theorem cardinal.sum_le_sum {ι : Type u_1} (f g : ι cardinal) (H : (i : ι), f i g i) :
theorem cardinal.mk_le_mk_mul_of_mk_preimage_le {α β : Type u} {c : cardinal} (f : α β) (hf : (b : β), cardinal.mk (f ⁻¹' {b}) c) :
* c
theorem cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le {α : Type u} {β : Type v} {c : cardinal} (f : α β) (hf : (b : β), (cardinal.mk (f ⁻¹' {b})).lift c) :
theorem cardinal.bdd_above_range {ι : Type u} (f : ι cardinal) :

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

@[protected, instance]
@[protected, instance]

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

theorem cardinal.supr_le_sum {ι : Type u_1} (f : ι cardinal) :
theorem cardinal.sum_le_supr_lift {ι : Type u} (f : ι cardinal) :
theorem cardinal.sum_le_supr {ι : Type u} (f : ι cardinal) :
theorem cardinal.sum_nat_eq_add_sum_succ (f : cardinal) :
= f 0 + cardinal.sum (λ (i : ), f (i + 1))
@[protected, simp]
theorem cardinal.supr_of_empty {ι : Sort u_1} (f : ι cardinal) [is_empty ι] :
supr f = 0

A variant of `csupr_of_empty` but with `0` on the RHS for convenience

@[simp]
theorem cardinal.lift_mk_shrink (α : Type u) [small α] :
@[simp]
theorem cardinal.lift_mk_shrink' (α : Type u) [small α] :
@[simp]
theorem cardinal.lift_mk_shrink'' (α : Type (max u v)) [small α] :
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.mk_pi {ι : Type u} (α : ι Type v) :
cardinal.mk (Π (i : ι), α i) = cardinal.prod (λ (i : ι), cardinal.mk (α i))
@[simp]
theorem cardinal.prod_const (ι : Type u) (a : cardinal) :
cardinal.prod (λ (i : ι), a) = a.lift ^ (cardinal.mk ι).lift
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) :
@[simp]
theorem cardinal.prod_eq_zero {ι : Type u_1} (f : ι cardinal) :
(i : ι), f i = 0
theorem cardinal.prod_ne_zero {ι : Type u_1} (f : ι cardinal) :
(i : ι), f i 0
@[simp]
theorem cardinal.lift_prod {ι : Type u} (c : ι cardinal) :
.lift = cardinal.prod (λ (i : ι), (c i).lift)
theorem cardinal.prod_eq_of_fintype {α : Type u} [fintype α] (f : α cardinal) :
= (finset.univ.prod (λ (i : α), f i)).lift
@[simp]
@[simp]
theorem cardinal.lift_infi {ι : Sort u_1} (f : ι cardinal) :
(infi f).lift = (i : ι), (f i).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]
@[simp]
theorem cardinal.lift_umax_eq {a : cardinal} {b : cardinal} :
a.lift = b.lift a.lift = b.lift
@[simp]
theorem cardinal.lift_min {a b : cardinal} :
b).lift =
@[simp]
theorem cardinal.lift_max {a b : cardinal} :
b).lift =
theorem cardinal.lift_Sup {s : set cardinal} (hs : bdd_above s) :

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

theorem cardinal.lift_supr {ι : Type v} {f : ι cardinal} (hf : bdd_above (set.range f)) :
(supr f).lift = (i : ι), (f i).lift

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

theorem cardinal.lift_supr_le {ι : Type v} {f : ι cardinal} {t : cardinal} (hf : bdd_above (set.range f)) (w : (i : ι), (f i).lift t) :
(supr 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`.

@[simp]
theorem cardinal.lift_supr_le_iff {ι : Type v} {f : ι cardinal} (hf : bdd_above (set.range f)) {t : cardinal} :
(supr f).lift t (i : ι), (f i).lift t
theorem cardinal.lift_supr_le_lift_supr {ι : Type v} {ι' : Type v'} {f : ι cardinal} {f' : ι' cardinal} (hf : bdd_above (set.range f)) (hf' : bdd_above (set.range f')) {g : ι ι'} (h : (i : ι), (f i).lift (f' (g i)).lift) :
(supr f).lift (supr 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.

theorem cardinal.lift_supr_le_lift_supr' {ι : Type v} {ι' : Type v'} {f : ι cardinal} {f' : ι' cardinal} (hf : bdd_above (set.range f)) (hf' : bdd_above (set.range f')) (g : ι ι') (h : (i : ι), (f i).lift (f' (g i)).lift) :
(supr f).lift (supr f').lift

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

`ℵ₀` is the smallest infinite cardinal.

Equations
theorem cardinal.mk_nat  :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

Properties about the cast from `ℕ`#

@[simp]
theorem cardinal.mk_fin (n : ) :
@[simp]
theorem cardinal.lift_nat_cast (n : ) :
@[simp]
theorem cardinal.lift_eq_nat_iff {a : cardinal} {n : } :
a.lift = n a = n
@[simp]
theorem cardinal.nat_eq_lift_iff {n : } {a : cardinal} :
n = a.lift n = a
@[simp]
theorem cardinal.lift_le_nat_iff {a : cardinal} {n : } :
@[simp]
theorem cardinal.nat_le_lift_iff {n : } {a : cardinal} :
@[simp]
theorem cardinal.lift_lt_nat_iff {a : cardinal} {n : } :
a.lift < n a < n
@[simp]
theorem cardinal.nat_lt_lift_iff {n : } {a : cardinal} :
n < a.lift n < a
theorem cardinal.mk_coe_finset {α : Type u} {s : finset α} :
= (s.card)
@[simp]
theorem cardinal.mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [fintype α] [has_zero β] :
theorem cardinal.mk_finsupp_of_fintype (α β : Type u) [fintype α] [has_zero β] :
theorem cardinal.card_le_of_finset {α : Type u_1} (s : finset α) :
@[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
@[protected, instance]
theorem cardinal.nat_cast_inj {m n : } :
m = n m = n
@[simp, norm_cast]
theorem cardinal.nat_succ (n : ) :
(n.succ) =
@[simp]
theorem cardinal.succ_zero  :
= 1
theorem cardinal.card_le_of {α : Type u} {n : } (H : (s : finset α), s.card 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
@[simp]
theorem cardinal.lt_aleph_0 {c : cardinal} :
(n : ), c = n
theorem cardinal.aleph_0_le {c : cardinal} :
(n : ), n c
@[simp]
theorem cardinal.mk_eq_nat_iff {α : Type u} {n : } :
theorem cardinal.lt_aleph_0_of_finite (α : Type u) [finite α] :
@[simp]
theorem cardinal.lt_aleph_0_iff_set_finite {α : Type u} {S : set α} :
theorem set.finite.lt_aleph_0 {α : Type u} {S : set α} :

Alias of the reverse direction of `cardinal.lt_aleph_0_iff_set_finite`.

@[simp]
theorem cardinal.lt_aleph_0_iff_subtype_finite {α : Type u} {p : α Prop} :
cardinal.mk {x // p x} < cardinal.aleph_0 {x : α | p x}.finite
theorem cardinal.mk_le_aleph_0_iff {α : Type u} :
@[simp]
theorem cardinal.mk_le_aleph_0 {α : Type u} [countable α] :
@[simp]
theorem cardinal.le_aleph_0_iff_set_countable {α : Type u} {s : set α} :
theorem set.countable.le_aleph_0 {α : Type u} {s : set α} :

Alias of the reverse direction of `cardinal.le_aleph_0_iff_set_countable`.

@[simp]
theorem cardinal.le_aleph_0_iff_subtype_countable {α : Type u} {p : α Prop} :
cardinal.mk {x // p x} cardinal.aleph_0 {x : α | p x}.countable
@[protected, instance]
Equations
theorem cardinal.nsmul_lt_aleph_0_iff {n : } {a : cardinal} :
n = 0

See also `cardinal.nsmul_lt_aleph_0_iff_of_ne_zero` if you already have `n ≠ 0`.

theorem cardinal.nsmul_lt_aleph_0_iff_of_ne_zero {n : } {a : cardinal} (h : n 0) :

See also `cardinal.nsmul_lt_aleph_0_iff` for a hypothesis-free version.

theorem cardinal.mul_lt_aleph_0_iff {a b : cardinal} :
a = 0 b = 0
theorem cardinal.aleph_0_le_mul_iff {a b : cardinal} :
a 0 b 0

See also `cardinal.aleph_0_le_mul_iff`.

theorem cardinal.aleph_0_le_mul_iff' {a b : cardinal} :
a 0 b 0

See also `cardinal.aleph_0_le_mul_iff'`.

theorem cardinal.mul_lt_aleph_0_iff_of_ne_zero {a b : cardinal} (ha : a 0) (hb : b 0) :
theorem cardinal.eq_one_iff_unique {α : Type u_1} :
= 1
theorem cardinal.infinite_iff {α : Type u} :
@[simp]
theorem cardinal.aleph_0_le_mk (α : Type u) [infinite α] :
@[simp]
theorem cardinal.mk_eq_aleph_0 (α : Type u_1) [countable α] [infinite α] :
theorem cardinal.denumerable_iff {α : Type u} :
@[simp]
theorem cardinal.mk_denumerable (α : Type u) [denumerable α] :
@[simp]
@[simp]
theorem cardinal.nat_mul_aleph_0 {n : } (hn : n 0) :
@[simp]
theorem cardinal.aleph_0_mul_nat {n : } (hn : n 0) :
@[simp]
theorem cardinal.add_le_aleph_0 {c₁ c₂ : cardinal} :
@[simp]
theorem cardinal.aleph_0_add_nat (n : ) :
@[simp]
theorem cardinal.nat_add_aleph_0 (n : ) :
noncomputable def cardinal.to_nat  :

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

Equations
theorem cardinal.to_nat_lt_of_lt_of_lt_aleph_0 {c d : cardinal} (hd : d < cardinal.aleph_0) (hcd : c < d) :
@[simp]
theorem cardinal.to_nat_cast (n : ) :

`to_nat` has a right-inverse: coercion.

theorem cardinal.exists_nat_eq_of_le_nat {c : cardinal} {n : } (h : c n) :
(m : ), m n c = m
@[simp]
theorem cardinal.mk_to_nat_of_infinite {α : Type u} [h : infinite α] :
@[simp]
theorem cardinal.mk_to_nat_eq_card {α : Type u} [fintype α] :
@[simp]
theorem cardinal.zero_to_nat  :
@[simp]
theorem cardinal.one_to_nat  :
theorem cardinal.to_nat_eq_iff {c : cardinal} {n : } (hn : n 0) :
c = n
@[simp]
theorem cardinal.to_nat_eq_one {c : cardinal} :
c = 1
@[simp]
theorem cardinal.to_nat_lift (c : cardinal) :
theorem cardinal.to_nat_congr {α : Type u} {β : Type v} (e : α β) :
@[simp]
@[simp]
theorem cardinal.to_nat_hom_apply (ᾰ : cardinal) :
noncomputable def cardinal.to_nat_hom  :

`cardinal.to_nat` as a `monoid_with_zero_hom`.

Equations
theorem cardinal.to_nat_finset_prod {α : Type u} (s : finset α) (f : α cardinal) :
cardinal.to_nat (s.prod (λ (i : α), f i)) = s.prod (λ (i : α), cardinal.to_nat (f i))
noncomputable def cardinal.to_part_enat  :

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

Equations
@[simp]
theorem cardinal.to_part_enat_cast (n : ) :
@[simp]
theorem cardinal.mk_to_part_enat_of_infinite {α : Type u} [h : infinite α] :
@[simp]
theorem cardinal.to_part_enat_mono {c c' : cardinal} (h : c c') :
theorem cardinal.to_part_enat_congr {α : Type u} {β : Type v} (e : α β) :
theorem cardinal.mk_int  :
theorem cardinal.sum_lt_prod {ι : Type u_1} (f g : ι cardinal) (H : (i : ι), f i < g i) :

König's theorem

@[simp]
theorem cardinal.mk_empty  :
@[simp]
theorem cardinal.mk_pempty  :
@[simp]
theorem cardinal.mk_punit  :
theorem cardinal.mk_unit  :
@[simp]
theorem cardinal.mk_singleton {α : Type u} (x : α) :
@[simp]
@[simp]
@[simp]
theorem cardinal.mk_vector (α : Type u) (n : ) :
theorem cardinal.mk_list_eq_sum_pow (α : Type u) :
cardinal.mk (list α) = cardinal.sum (λ (n : ), ^ n)
theorem cardinal.mk_quot_le {α : Type u} {r : α α Prop} :
cardinal.mk (quot r)
theorem cardinal.mk_quotient_le {α : Type u} {s : setoid α} :
theorem cardinal.mk_subtype_le_of_subset {α : Type u} {p q : α Prop} (h : ⦃x : α⦄, p x q x) :
@[simp]
theorem cardinal.mk_emptyc (α : Type u) :
theorem cardinal.mk_emptyc_iff {α : Type u} {s : set α} :
s =
@[simp]
theorem cardinal.mk_univ {α : Type u} :
theorem cardinal.mk_image_le {α β : Type u} {f : α β} {s : set α} :
theorem cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : α β} {s : set α} :
theorem cardinal.mk_range_le {α β : Type u} {f : α β} :
theorem cardinal.mk_range_le_lift {α : Type u} {β : Type v} {f : α β} :
theorem cardinal.mk_range_eq {α β : Type u} (f : α β) (h : function.injective f) :
theorem cardinal.mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α β} (hf : function.injective f) :
theorem cardinal.mk_range_eq_lift {α : Type u} {β : Type v} {f : α β} (hf : function.injective f) :
theorem cardinal.mk_image_eq {α β : Type u} {f : α β} {s : set α} (hf : function.injective f) :
theorem cardinal.mk_Union_le_sum_mk {α ι : Type u} {f : ι set α} :
cardinal.mk ( (i : ι), f i) cardinal.sum (λ (i : ι), cardinal.mk (f i))
theorem cardinal.mk_Union_eq_sum_mk {α ι : Type u} {f : ι set α} (h : (i j : ι), i j disjoint (f i) (f j)) :
cardinal.mk ( (i : ι), f i) = cardinal.sum (λ (i : ι), cardinal.mk (f i))
theorem cardinal.mk_Union_le {α ι : Type u} (f : ι set α) :
cardinal.mk ( (i : ι), f i) * (i : ι), cardinal.mk (f i)
theorem cardinal.mk_sUnion_le {α : Type u} (A : set (set α)) :
theorem cardinal.mk_bUnion_le {ι α : Type u} (A : ι set α) (s : set ι) :
cardinal.mk ( (x : ι) (H : x s), A x) * (x : s), cardinal.mk (A x.val)
theorem cardinal.finset_card_lt_aleph_0 {α : Type u} (s : finset α) :
theorem cardinal.mk_set_eq_nat_iff_finset {α : Type u_1} {s : set α} {n : } :
(t : finset α), t = s t.card = n
theorem cardinal.mk_eq_nat_iff_finset {α : Type u} {n : } :
(t : finset α), t.card = n
theorem cardinal.mk_eq_nat_iff_fintype {α : Type u} {n : } :
(h : fintype α),
theorem cardinal.mk_union_add_mk_inter {α : Type u} {S T : set α} :
theorem cardinal.mk_union_le {α : Type u} (S T : set α) :

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) :
theorem cardinal.mk_insert {α : Type u} {s : set α} {a : α} (h : a s) :
=
theorem cardinal.mk_sum_compl {α : Type u_1} (s : set α) :
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 x q x) :
cardinal.mk {x // p x} cardinal.mk {x // q x}
theorem cardinal.le_mk_diff_add_mk {α : Type u} (S T : set α) :
theorem cardinal.mk_diff_add_mk {α : Type u} {S T : set α} (h : T S) :
theorem cardinal.mk_union_le_aleph_0 {α : Type u_1} {P Q : set α} :
theorem cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : α β) (s : set α) (h : function.injective f) :
theorem cardinal.mk_image_eq_of_inj_on_lift {α : Type u} {β : Type v} (f : α β) (s : set α) (h : s) :
theorem cardinal.mk_image_eq_of_inj_on {α β : Type u} (f : α β) (s : set α) (h : s) :
theorem cardinal.mk_subtype_of_equiv {α β : Type u} (p : β Prop) (e : α β) :
cardinal.mk {a // p (e a)} = cardinal.mk {b // p b}
theorem cardinal.mk_sep {α : Type u} (s : set α) (t : α Prop) :
cardinal.mk {x ∈ s | t x} = cardinal.mk {x : s | t x.val}
theorem cardinal.mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α β) (s : set β) (h : function.injective f) :
theorem cardinal.mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α β) (s : set β) (h : s ) :
theorem cardinal.mk_preimage_of_injective_of_subset_range_lift {α : Type u} {β : Type v} (f : α β) (s : set β) (h : function.injective f) (h2 : s ) :
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 ) :
theorem cardinal.mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α β) {s : set α} {t : set β} (h : t f '' s) :
(cardinal.mk t).lift (cardinal.mk {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) :
cardinal.mk {x ∈ s | f x t}
theorem cardinal.le_mk_iff_exists_subset {c : cardinal} {α : Type u} {s : set α} :
(p : set α), p s
theorem cardinal.two_le_iff {α : Type u} :
2 (x y : α), x y
theorem cardinal.two_le_iff' {α : Type u} (x : α) :
2 (y : α), y x
theorem cardinal.mk_eq_two_iff {α : Type u} :
= 2 (x y : α), x y {x, y} = set.univ
theorem cardinal.mk_eq_two_iff' {α : Type u} (x : α) :
= 2 ∃! (y : α), y x
theorem cardinal.exists_not_mem_of_length_lt {α : Type u_1} (l : list α) (h : (l.length) < ) :
(z : α), z l
theorem cardinal.three_le {α : Type u_1} (h : 3 ) (x y : α) :
(z : α), z x z y
noncomputable def cardinal.powerlt (a b : cardinal) :

The function `a ^< b`, defined as the supremum of `a ^ c` for `c < b`.

Equations
theorem cardinal.le_powerlt {b c : cardinal} (a : cardinal) (h : c < b) :
a ^ c a ^< b
theorem cardinal.powerlt_le {a b c : cardinal} :
a ^< b c (x : cardinal), x < b a ^ x c
theorem cardinal.powerlt_le_powerlt_left {a b c : cardinal} (h : b c) :
a ^< b a ^< c
theorem cardinal.powerlt_mono_left (a : cardinal) :
monotone (λ (c : cardinal), a ^< c)
theorem cardinal.powerlt_succ {a b : cardinal} (h : a 0) :
a ^< = a ^ b
theorem cardinal.powerlt_min {a b c : cardinal} :
a ^< = linear_order.min (a ^< b) (a ^< c)
theorem cardinal.powerlt_max {a b c : cardinal} :
a ^< = linear_order.max (a ^< b) (a ^< c)
theorem cardinal.zero_powerlt {a : cardinal} (h : a 0) :
0 ^< a = 1
@[simp]
theorem cardinal.powerlt_zero {a : cardinal} :
a ^< 0 = 0

Extension for the `positivity` tactic: The cardinal power of a positive cardinal is positive.