mathlib3 documentation

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 #

Main instances #

Main Statements #

Implementation notes #

References #

Tags #

cardinal number, cardinal arithmetic, cardinal exponentiation, aleph, 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
Instances for cardinal
source
def cardinal.mk  :
Type u → cardinal

The cardinal number of a type

Equations
Instances for cardinal.mk
source
@[protected, instance]
def cardinal.can_lift_cardinal_Type  :
can_lift cardinal (Type u) cardinal.mk (λ (_x : cardinal), true)
Equations
source
theorem cardinal.induction_on {p : cardinal → Prop} (c : cardinal) (h : ∀ (α : Type u_1), p (cardinal.mk α)) :
p c
source
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₂
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 (cardinal.mk α) (cardinal.mk β) (cardinal.mk γ)) :
p c₁ c₂ c₃
source
@[protected]
theorem cardinal.eq {α β : Type u} :
cardinal.mk α = cardinal.mk β ↔ nonempty (α ≃ β)
source
@[simp]
theorem cardinal.mk_def (α : Type u) :
⟦α⟧ = cardinal.mk α
source
@[simp]
theorem cardinal.mk_out (c : cardinal) :
cardinal.mk (quotient.out c) = c
source
noncomputable def cardinal.out_mk_equiv {α : Type v} :
quotient.out (cardinal.mk α) ≃ α

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

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

Alias of cardinal.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 (cardinal.mk α) = cardinal.mk (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) :
cardinal.mk (ulift α) = (cardinal.mk α).lift
source
@[simp]
theorem cardinal.lift_umax  :
cardinal.lift = cardinal.lift

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.

source
@[simp]
theorem cardinal.lift_umax'  :
cardinal.lift = cardinal.lift

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.

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

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

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

A cardinal lifted to the same universe equals itself.

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

A cardinal lifted to the zero universe equals itself.

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
@[protected, instance]
def cardinal.partial_order  :
partial_order cardinal
Equations
source
@[protected, instance]
noncomputable def cardinal.linear_order  :
linear_order cardinal
Equations
source
theorem cardinal.le_def (α β : Type u) :
cardinal.mk α ≤ cardinal.mk β ↔ nonempty (α ↪ β)
source
theorem cardinal.mk_le_of_injective {α β : Type u} {f : α → β} (hf : function.injective f) :
cardinal.mk α ≤ cardinal.mk β
source
theorem function.embedding.cardinal_le {α β : Type u} (f : α ↪ β) :
cardinal.mk α ≤ cardinal.mk β
source
theorem cardinal.mk_le_of_surjective {α β : Type u} {f : α → β} (hf : function.surjective f) :
cardinal.mk β ≤ cardinal.mk α
source
theorem cardinal.le_mk_iff_exists_set {c : cardinal} {α : Type u} :
c ≤ cardinal.mk α ↔ ∃ (p : set α), cardinal.mk ↥p = c
source
theorem cardinal.mk_subtype_le {α : Type u} (p : α → Prop) :
cardinal.mk (subtype p) ≤ cardinal.mk α
source
theorem cardinal.mk_set_le {α : Type u} (s : set α) :
cardinal.mk ↥s ≤ cardinal.mk α
source
theorem cardinal.out_embedding {c c' : cardinal} :
c ≤ c' ↔ nonempty (quotient.out c ↪ quotient.out c')
source
theorem cardinal.lift_mk_le {α : Type u} {β : Type v} :
(cardinal.mk α).lift ≤ (cardinal.mk β).lift ↔ nonempty (α ↪ β)
source
theorem cardinal.lift_mk_le' {α : Type u} {β : Type v} :
(cardinal.mk α).lift ≤ (cardinal.mk β).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} :
(cardinal.mk α).lift = (cardinal.mk β).lift ↔ nonempty (α ≃ β)
source
theorem cardinal.lift_mk_eq' {α : Type u} {β : Type v} :
(cardinal.mk α).lift = (cardinal.mk β).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
theorem cardinal.lift_strict_mono  :
strict_mono cardinal.lift
source
theorem cardinal.lift_monotone  :
monotone cardinal.lift
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 α] :
cardinal.mk α = 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} :
cardinal.mk α = 0 ↔ is_empty α
source
theorem cardinal.mk_ne_zero_iff {α : Type u} :
cardinal.mk α ≠ 0 ↔ nonempty α
source
@[simp]
theorem cardinal.mk_ne_zero (α : Type u) [nonempty α] :
cardinal.mk α ≠ 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 α] :
cardinal.mk α = 1
source
theorem cardinal.le_one_iff_subsingleton {α : Type u} :
cardinal.mk α ≤ 1 ↔ subsingleton α
source
@[simp]
theorem cardinal.mk_le_one_iff_set_subsingleton {α : Type u} {s : set α} :
cardinal.mk ↥s ≤ 1 ↔ s.subsingleton
source
theorem set.subsingleton.cardinal_mk_le_one {α : Type u} {s : set α} :
s.subsingleton → cardinal.mk ↥s ≤ 1

Alias of the reverse direction of cardinal.mk_le_one_iff_set_subsingleton.

source
@[protected, instance]
def cardinal.has_add  :
has_add cardinal
Equations
source
theorem cardinal.add_def (α β : Type u) :
cardinal.mk α + cardinal.mk β = cardinal.mk (α ⊕ β)
source
@[protected, instance]
def cardinal.has_nat_cast  :
has_nat_cast cardinal
Equations
source
@[simp]
theorem cardinal.mk_sum (α : Type u) (β : Type v) :
cardinal.mk (α ⊕ β) = (cardinal.mk α).lift + (cardinal.mk β).lift
source
@[simp]
theorem cardinal.mk_option {α : Type u} :
cardinal.mk (option α) = cardinal.mk α + 1
source
@[simp]
theorem cardinal.mk_psum (α : Type u) (β : Type v) :
cardinal.mk (psum α β) = (cardinal.mk α).lift + (cardinal.mk β).lift
source
@[simp]
theorem cardinal.mk_fintype (α : Type u) [fintype α] :
cardinal.mk α = ↑(fintype.card α)
source
@[protected, instance]
def cardinal.has_mul  :
has_mul cardinal
Equations
source
theorem cardinal.mul_def (α β : Type u) :
cardinal.mk α * cardinal.mk β = cardinal.mk (α × β)
source
@[simp]
theorem cardinal.mk_prod (α : Type u) (β : Type v) :
cardinal.mk (α × β) = (cardinal.mk α).lift * (cardinal.mk β).lift
source
@[protected, instance]
def cardinal.has_pow  :
has_pow cardinal cardinal

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

Equations
source
theorem cardinal.power_def (α β : Type u_1) :
cardinal.mk α ^ cardinal.mk β = cardinal.mk (β → α)
source
theorem cardinal.mk_arrow (α : Type u) (β : Type v) :
cardinal.mk (α → β) = (cardinal.mk β).lift ^ (cardinal.mk α).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  :
cardinal.mk bool = 2
source
@[simp]
theorem cardinal.mk_Prop  :
cardinal.mk 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 (a : cardinal) (n : ℕ) :
a ^ ↑n = a ^ 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} :
cardinal.mk (set α) = 2 ^ cardinal.mk α
source
@[simp]
theorem cardinal.mk_powerset {α : Type u} (s : set α) :
cardinal.mk (↥𝒫s) = 2 ^ cardinal.mk ↥s

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

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, instance]
def cardinal.add_covariant_class  :
covariant_class cardinal cardinal has_add.add has_le.le
source
@[protected, instance]
def cardinal.add_swap_covariant_class  :
covariant_class cardinal cardinal (function.swap has_add.add) has_le.le
source
@[protected, instance]
def cardinal.canonically_ordered_comm_semiring  :
canonically_ordered_comm_semiring cardinal
Equations
source
@[protected, instance]
noncomputable def cardinal.canonically_linear_ordered_add_monoid  :
canonically_linear_ordered_add_monoid cardinal
Equations
source
@[protected, instance]
def cardinal.canonically_ordered_add_monoid  :
canonically_ordered_add_monoid cardinal
Equations
source
@[protected, instance]
noncomputable def cardinal.linear_ordered_comm_monoid_with_zero  :
linear_ordered_comm_monoid_with_zero cardinal
Equations
source
@[protected, instance]
def cardinal.comm_monoid_with_zero  :
comm_monoid_with_zero cardinal
Equations
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.distrib_lattice  :
distrib_lattice cardinal
Equations
source
theorem cardinal.one_lt_iff_nontrivial {α : Type u} :
1 < cardinal.mk α ↔ nontrivial α
source
theorem cardinal.power_le_max_power_one {a b c : cardinal} (h : b ≤ c) :
a ^ b ≤ linear_order.max (a ^ c) 1
source
theorem cardinal.power_le_power_right {a b c : cardinal} :
a ≤ b → a ^ c ≤ b ^ c
source
theorem cardinal.power_pos {a : cardinal} (b : cardinal) (ha : 0 < a) :
0 < a ^ b
source
@[protected]
theorem cardinal.lt_wf  :
well_founded has_lt.lt
source
@[protected, instance]
def cardinal.has_well_founded  :
has_well_founded cardinal
Equations
source
@[protected, instance]
def cardinal.wo  :
is_well_order cardinal has_lt.lt
source
@[protected, instance]
noncomputable def cardinal.conditionally_complete_linear_order_bot  :
conditionally_complete_linear_order_bot cardinal
Equations
source
@[simp]
theorem cardinal.Inf_empty  :
has_Inf.Inf ∅ = 0
source
@[protected, instance]
noncomputable def cardinal.succ_order  :
succ_order cardinal

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

Equations
source
theorem cardinal.succ_def (c : cardinal) :
order.succ c = has_Inf.Inf {c' : cardinal | c < c'}
source
theorem cardinal.succ_pos (c : cardinal) :
0 < order.succ c
source
theorem cardinal.succ_ne_zero (c : cardinal) :
order.succ c ≠ 0
source
theorem cardinal.add_one_le_succ (c : cardinal) :
c + 1 ≤ order.succ c
source
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
source
@[protected]
theorem cardinal.is_limit.ne_zero {c : cardinal} (h : c.is_limit) :
c ≠ 0
source
@[protected]
theorem cardinal.is_limit.is_succ_limit {c : cardinal} (h : c.is_limit) :
order.is_succ_limit c
source
theorem cardinal.is_limit.succ_lt {x c : cardinal} (h : c.is_limit) :
x < c → order.succ x < c
source
theorem cardinal.is_succ_limit_zero  :
order.is_succ_limit 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) :
cardinal.mk (Σ (i : ι), f i) = cardinal.sum (λ (i : ι), cardinal.mk (f i))
source
@[simp]
theorem cardinal.sum_const (ι : Type u) (a : cardinal) :
cardinal.sum (λ (i : ι), a) = (cardinal.mk ι).lift * a.lift
source
theorem cardinal.sum_const' (ι : Type u) (a : cardinal) :
cardinal.sum (λ (_x : ι), a) = cardinal.mk ι * a
source
@[simp]
theorem cardinal.sum_add_distrib {ι : Type u_1} (f g : ι → cardinal) :
cardinal.sum (f + g) = cardinal.sum f + cardinal.sum g
source
@[simp]
theorem cardinal.sum_add_distrib' {ι : Type u_1} (f g : ι → cardinal) :
cardinal.sum (λ (i : ι), f i + g i) = cardinal.sum f + cardinal.sum g
source
@[simp]
theorem cardinal.lift_sum {ι : Type u} (f : ι → cardinal) :
(cardinal.sum f).lift = cardinal.sum (λ (i : ι), (f i).lift)
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 : β), cardinal.mk ↥(f ⁻¹' {b}) ≤ c) :
cardinal.mk α ≤ cardinal.mk β * c
source
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) :
(cardinal.mk α).lift ≤ (cardinal.mk β).lift * 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
@[protected, instance]
def cardinal.set.Iio.small (a : cardinal) :
small ↥(set.Iio 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
theorem cardinal.bdd_above_of_small (s : set cardinal) [h : small ↥s] :
bdd_above s
source
theorem cardinal.bdd_above_image (f : cardinal → cardinal) {s : set cardinal} (hs : bdd_above s) :
bdd_above (f '' s)
source
theorem cardinal.bdd_above_range_comp {ι : Type u} {f : ι → cardinal} (hf : bdd_above (set.range f)) (g : cardinal → cardinal) :
bdd_above (set.range (g ∘ f))
source
theorem cardinal.supr_le_sum {ι : Type u_1} (f : ι → cardinal) :
supr f ≤ cardinal.sum f
source
theorem cardinal.sum_le_supr_lift {ι : Type u} (f : ι → cardinal) :
cardinal.sum f ≤ (cardinal.mk ι).lift * supr f
source
theorem cardinal.sum_le_supr {ι : Type u} (f : ι → cardinal) :
cardinal.sum f ≤ cardinal.mk ι * supr f
source
theorem cardinal.sum_nat_eq_add_sum_succ (f : ℕ → cardinal) :
cardinal.sum f = f 0 + cardinal.sum (λ (i : ℕ), f (i + 1))
source
@[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

source
@[simp]
theorem cardinal.lift_mk_shrink (α : Type u) [small α] :
(cardinal.mk (shrink α)).lift = (cardinal.mk α).lift
source
@[simp]
theorem cardinal.lift_mk_shrink' (α : Type u) [small α] :
(cardinal.mk (shrink α)).lift = (cardinal.mk α).lift
source
@[simp]
theorem cardinal.lift_mk_shrink'' (α : Type (max u v)) [small α] :
(cardinal.mk (shrink α)).lift = cardinal.mk α
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) :
cardinal.mk (Π (i : ι), α i) = cardinal.prod (λ (i : ι), cardinal.mk (α i))
source
@[simp]
theorem cardinal.prod_const (ι : Type u) (a : cardinal) :
cardinal.prod (λ (i : ι), a) = a.lift ^ (cardinal.mk ι).lift
source
theorem cardinal.prod_const' (ι : Type u) (a : cardinal) :
cardinal.prod (λ (_x : ι), a) = a ^ cardinal.mk ι
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
theorem cardinal.prod_eq_of_fintype {α : Type u} [fintype α] (f : α → cardinal) :
cardinal.prod f = (finset.univ.prod (λ (i : α), f i)).lift
source
@[simp]
theorem cardinal.lift_Inf (s : set cardinal) :
(has_Inf.Inf s).lift = has_Inf.Inf (cardinal.lift '' s)
source
@[simp]
theorem cardinal.lift_infi {ι : Sort u_1} (f : ι → cardinal) :
(infi f).lift = ⨅ (i : ι), (f i).lift
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) :
(order.succ a).lift = order.succ a.lift
source
@[simp]
theorem cardinal.lift_umax_eq {a : cardinal} {b : cardinal} :
a.lift = b.lift ↔ a.lift = b.lift
source
@[simp]
theorem cardinal.lift_min {a b : cardinal} :
(linear_order.min a b).lift = linear_order.min a.lift b.lift
source
@[simp]
theorem cardinal.lift_max {a b : cardinal} :
(linear_order.max a b).lift = linear_order.max a.lift b.lift
source
theorem cardinal.lift_Sup {s : set cardinal} (hs : bdd_above s) :
(has_Sup.Sup s).lift = has_Sup.Sup (cardinal.lift '' s)

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

source
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.

source
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.

source
@[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
source
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.

source
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.

source
def cardinal.aleph_0  :
cardinal

ℵ₀ is the smallest infinite cardinal.

Equations
source
theorem cardinal.mk_nat  :
cardinal.mk ℕ = cardinal.aleph_0
source
theorem cardinal.aleph_0_ne_zero  :
cardinal.aleph_0 ≠ 0
source
theorem cardinal.aleph_0_pos  :
0 < cardinal.aleph_0
source
@[simp]
theorem cardinal.lift_aleph_0  :
cardinal.aleph_0.lift = cardinal.aleph_0
source
@[simp]
theorem cardinal.aleph_0_le_lift {c : cardinal} :
cardinal.aleph_0 ≤ c.lift ↔ cardinal.aleph_0 ≤ c
source
@[simp]
theorem cardinal.lift_le_aleph_0 {c : cardinal} :
c.lift ≤ cardinal.aleph_0 ↔ c ≤ cardinal.aleph_0
source
@[simp]
theorem cardinal.aleph_0_lt_lift {c : cardinal} :
cardinal.aleph_0 < c.lift ↔ cardinal.aleph_0 < c
source
@[simp]
theorem cardinal.lift_lt_aleph_0 {c : cardinal} :
c.lift < cardinal.aleph_0 ↔ c < cardinal.aleph_0

Properties about the cast from ℕ #

source
@[simp]
theorem cardinal.mk_fin (n : ℕ) :
cardinal.mk (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
@[simp]
theorem cardinal.lift_le_nat_iff {a : cardinal} {n : ℕ} :
a.lift ≤ ↑n ↔ a ≤ ↑n
source
@[simp]
theorem cardinal.nat_le_lift_iff {n : ℕ} {a : cardinal} :
↑n ≤ a.lift ↔ ↑n ≤ a
source
@[simp]
theorem cardinal.lift_lt_nat_iff {a : cardinal} {n : ℕ} :
a.lift < ↑n ↔ a < ↑n
source
@[simp]
theorem cardinal.nat_lt_lift_iff {n : ℕ} {a : cardinal} :
↑n < a.lift ↔ ↑n < a
source
theorem cardinal.lift_mk_fin (n : ℕ) :
(cardinal.mk (fin n)).lift = ↑n
source
theorem cardinal.mk_coe_finset {α : Type u} {s : finset α} :
cardinal.mk ↥s = ↑(s.card)
source
theorem cardinal.mk_finset_of_fintype {α : Type u} [fintype α] :
cardinal.mk (finset α) = 2 ^ fintype.card α
source
@[simp]
theorem cardinal.mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [fintype α] [has_zero β] :
cardinal.mk (α →₀ β) = (cardinal.mk β).lift ^ fintype.card α
source
theorem cardinal.mk_finsupp_of_fintype (α β : Type u) [fintype α] [has_zero β] :
cardinal.mk (α →₀ β) = cardinal.mk β ^ fintype.card α
source
theorem cardinal.card_le_of_finset {α : Type u_1} (s : finset α) :
↑(s.card) ≤ cardinal.mk α
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) = order.succ ↑n
source
@[simp]
theorem cardinal.succ_zero  :
order.succ 0 = 1
source
theorem cardinal.card_le_of {α : Type u} {n : ℕ} (H : ∀ (s : finset α), s.card ≤ n) :
cardinal.mk α ≤ ↑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_aleph_0 (n : ℕ) :
↑n < cardinal.aleph_0
source
@[simp]
theorem cardinal.one_lt_aleph_0  :
1 < cardinal.aleph_0
source
theorem cardinal.one_le_aleph_0  :
1 ≤ cardinal.aleph_0
source
theorem cardinal.lt_aleph_0 {c : cardinal} :
c < cardinal.aleph_0 ↔ ∃ (n : ℕ), c = ↑n
source
theorem cardinal.aleph_0_le {c : cardinal} :
cardinal.aleph_0 ≤ c ↔ ∀ (n : ℕ), ↑n ≤ c
source
theorem cardinal.is_succ_limit_aleph_0  :
order.is_succ_limit cardinal.aleph_0
source
theorem cardinal.is_limit_aleph_0  :
cardinal.aleph_0.is_limit
source
theorem cardinal.is_limit.aleph_0_le {c : cardinal} (h : c.is_limit) :
cardinal.aleph_0 ≤ c
source
@[simp]
theorem cardinal.range_nat_cast  :
set.range coe = set.Iio cardinal.aleph_0
source
theorem cardinal.mk_eq_nat_iff {α : Type u} {n : ℕ} :
cardinal.mk α = ↑n ↔ nonempty (α ≃ fin n)
source
theorem cardinal.lt_aleph_0_iff_finite {α : Type u} :
cardinal.mk α < cardinal.aleph_0 ↔ finite α
source
theorem cardinal.lt_aleph_0_iff_fintype {α : Type u} :
cardinal.mk α < cardinal.aleph_0 ↔ nonempty (fintype α)
source
theorem cardinal.lt_aleph_0_of_finite (α : Type u) [finite α] :
cardinal.mk α < cardinal.aleph_0
source
@[simp]
theorem cardinal.lt_aleph_0_iff_set_finite {α : Type u} {S : set α} :
cardinal.mk ↥S < cardinal.aleph_0 ↔ S.finite
source
theorem set.finite.lt_aleph_0 {α : Type u} {S : set α} :
S.finite → cardinal.mk ↥S < cardinal.aleph_0

Alias of the reverse direction of cardinal.lt_aleph_0_iff_set_finite.

source
@[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
source
theorem cardinal.mk_le_aleph_0_iff {α : Type u} :
cardinal.mk α ≤ cardinal.aleph_0 ↔ countable α
source
@[simp]
theorem cardinal.mk_le_aleph_0 {α : Type u} [countable α] :
cardinal.mk α ≤ cardinal.aleph_0
source
@[simp]
theorem cardinal.le_aleph_0_iff_set_countable {α : Type u} {s : set α} :
cardinal.mk ↥s ≤ cardinal.aleph_0 ↔ s.countable
source
theorem set.countable.le_aleph_0 {α : Type u} {s : set α} :
s.countable → cardinal.mk ↥s ≤ cardinal.aleph_0

Alias of the reverse direction of cardinal.le_aleph_0_iff_set_countable.

source
@[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
source
@[protected, instance]
def cardinal.can_lift_cardinal_nat  :
can_lift cardinal ℕ coe (λ (x : cardinal), x < cardinal.aleph_0)
Equations
source
theorem cardinal.add_lt_aleph_0 {a b : cardinal} (ha : a < cardinal.aleph_0) (hb : b < cardinal.aleph_0) :
a + b < cardinal.aleph_0
source
theorem cardinal.add_lt_aleph_0_iff {a b : cardinal} :
a + b < cardinal.aleph_0 ↔ a < cardinal.aleph_0 ∧ b < cardinal.aleph_0
source
theorem cardinal.aleph_0_le_add_iff {a b : cardinal} :
cardinal.aleph_0 ≤ a + b ↔ cardinal.aleph_0 ≤ a ∨ cardinal.aleph_0 ≤ b
source
theorem cardinal.nsmul_lt_aleph_0_iff {n : ℕ} {a : cardinal} :
n • a < cardinal.aleph_0 ↔ n = 0 ∨ a < cardinal.aleph_0

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

source
theorem cardinal.nsmul_lt_aleph_0_iff_of_ne_zero {n : ℕ} {a : cardinal} (h : n ≠ 0) :
n • a < cardinal.aleph_0 ↔ a < cardinal.aleph_0

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

source
theorem cardinal.mul_lt_aleph_0 {a b : cardinal} (ha : a < cardinal.aleph_0) (hb : b < cardinal.aleph_0) :
a * b < cardinal.aleph_0
source
theorem cardinal.mul_lt_aleph_0_iff {a b : cardinal} :
a * b < cardinal.aleph_0 ↔ a = 0 ∨ b = 0 ∨ a < cardinal.aleph_0 ∧ b < cardinal.aleph_0
source
theorem cardinal.aleph_0_le_mul_iff {a b : cardinal} :
cardinal.aleph_0 ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (cardinal.aleph_0 ≤ a ∨ cardinal.aleph_0 ≤ b)

See also cardinal.aleph_0_le_mul_iff.

source
theorem cardinal.aleph_0_le_mul_iff' {a b : cardinal} :
cardinal.aleph_0 ≤ a * b ↔ a ≠ 0 ∧ cardinal.aleph_0 ≤ b ∨ cardinal.aleph_0 ≤ a ∧ b ≠ 0

See also cardinal.aleph_0_le_mul_iff'.

source
theorem cardinal.mul_lt_aleph_0_iff_of_ne_zero {a b : cardinal} (ha : a ≠ 0) (hb : b ≠ 0) :
a * b < cardinal.aleph_0 ↔ a < cardinal.aleph_0 ∧ b < cardinal.aleph_0
source
theorem cardinal.power_lt_aleph_0 {a b : cardinal} (ha : a < cardinal.aleph_0) (hb : b < cardinal.aleph_0) :
a ^ b < cardinal.aleph_0
source
theorem cardinal.eq_one_iff_unique {α : Type u_1} :
cardinal.mk α = 1 ↔ subsingleton α ∧ nonempty α
source
theorem cardinal.infinite_iff {α : Type u} :
infinite α ↔ cardinal.aleph_0 ≤ cardinal.mk α
source
@[simp]
theorem cardinal.aleph_0_le_mk (α : Type u) [infinite α] :
cardinal.aleph_0 ≤ cardinal.mk α
source
@[simp]
theorem cardinal.mk_eq_aleph_0 (α : Type u_1) [countable α] [infinite α] :
cardinal.mk α = cardinal.aleph_0
source
theorem cardinal.denumerable_iff {α : Type u} :
nonempty (denumerable α) ↔ cardinal.mk α = cardinal.aleph_0
source
@[simp]
theorem cardinal.mk_denumerable (α : Type u) [denumerable α] :
cardinal.mk α = cardinal.aleph_0
source
@[simp]
theorem cardinal.aleph_0_add_aleph_0  :
cardinal.aleph_0 + cardinal.aleph_0 = cardinal.aleph_0
source
theorem cardinal.aleph_0_mul_aleph_0  :
cardinal.aleph_0 * cardinal.aleph_0 = cardinal.aleph_0
source
@[simp]
theorem cardinal.nat_mul_aleph_0 {n : ℕ} (hn : n ≠ 0) :
↑n * cardinal.aleph_0 = cardinal.aleph_0
source
@[simp]
theorem cardinal.aleph_0_mul_nat {n : ℕ} (hn : n ≠ 0) :
cardinal.aleph_0 * ↑n = cardinal.aleph_0
source
@[simp]
theorem cardinal.add_le_aleph_0 {c₁ c₂ : cardinal} :
c₁ + c₂ ≤ cardinal.aleph_0 ↔ c₁ ≤ cardinal.aleph_0 ∧ c₂ ≤ cardinal.aleph_0
source
@[simp]
theorem cardinal.aleph_0_add_nat (n : ℕ) :
cardinal.aleph_0 + ↑n = cardinal.aleph_0
source
@[simp]
theorem cardinal.nat_add_aleph_0 (n : ℕ) :
↑n + cardinal.aleph_0 = cardinal.aleph_0
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_aleph_0 {c : cardinal} (h : c < cardinal.aleph_0) :
⇑cardinal.to_nat c = classical.some _
source
theorem cardinal.to_nat_apply_of_aleph_0_le {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
⇑cardinal.to_nat c = 0
source
theorem cardinal.cast_to_nat_of_lt_aleph_0 {c : cardinal} (h : c < cardinal.aleph_0) :
↑(⇑cardinal.to_nat c) = c
source
theorem cardinal.cast_to_nat_of_aleph_0_le {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
↑(⇑cardinal.to_nat c) = 0
source
theorem cardinal.to_nat_eq_iff_eq_of_lt_aleph_0 {c d : cardinal} (hc : c < cardinal.aleph_0) (hd : d < cardinal.aleph_0) :
⇑cardinal.to_nat c = ⇑cardinal.to_nat d ↔ c = d
source
theorem cardinal.to_nat_le_iff_le_of_lt_aleph_0 {c d : cardinal} (hc : c < cardinal.aleph_0) (hd : d < cardinal.aleph_0) :
⇑cardinal.to_nat c ≤ ⇑cardinal.to_nat d ↔ c ≤ d
source
theorem cardinal.to_nat_lt_iff_lt_of_lt_aleph_0 {c d : cardinal} (hc : c < cardinal.aleph_0) (hd : d < cardinal.aleph_0) :
⇑cardinal.to_nat c < ⇑cardinal.to_nat d ↔ c < d
source
theorem cardinal.to_nat_le_of_le_of_lt_aleph_0 {c d : cardinal} (hd : d < cardinal.aleph_0) (hcd : c ≤ d) :
⇑cardinal.to_nat c ≤ ⇑cardinal.to_nat d
source
theorem cardinal.to_nat_lt_of_lt_of_lt_aleph_0 {c d : cardinal} (hd : d < cardinal.aleph_0) (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
theorem cardinal.exists_nat_eq_of_le_nat {c : cardinal} {n : ℕ} (h : c ≤ ↑n) :
∃ (m : ℕ), m ≤ n ∧ c = ↑m
source
@[simp]
theorem cardinal.mk_to_nat_of_infinite {α : Type u} [h : infinite α] :
⇑cardinal.to_nat (cardinal.mk α) = 0
source
@[simp]
theorem cardinal.aleph_0_to_nat  :
⇑cardinal.to_nat cardinal.aleph_0 = 0
source
theorem cardinal.mk_to_nat_eq_card {α : Type u} [fintype α] :
⇑cardinal.to_nat (cardinal.mk α) = 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
theorem cardinal.to_nat_eq_iff {c : cardinal} {n : ℕ} (hn : n ≠ 0) :
⇑cardinal.to_nat c = n ↔ c = ↑n
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 (cardinal.mk α) = 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.mk α) = ⇑cardinal.to_nat (cardinal.mk β)
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_hom_apply (ᾰ : cardinal) :
⇑cardinal.to_nat_hom ᾰ = ⇑cardinal.to_nat ᾰ
source
noncomputable def cardinal.to_nat_hom  :
cardinal →*₀ ℕ

cardinal.to_nat as a monoid_with_zero_hom.

Equations
source
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))
source
@[simp]
theorem cardinal.to_nat_add_of_lt_aleph_0 {a : cardinal} {b : cardinal} (ha : a < cardinal.aleph_0) (hb : b < cardinal.aleph_0) :
⇑cardinal.to_nat (a.lift + b.lift) = ⇑cardinal.to_nat a + ⇑cardinal.to_nat b
source
noncomputable def cardinal.to_part_enat  :
cardinal →+ part_enat

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

Equations
source
theorem cardinal.to_part_enat_apply_of_lt_aleph_0 {c : cardinal} (h : c < cardinal.aleph_0) :
⇑cardinal.to_part_enat c = ↑(⇑cardinal.to_nat c)
source
theorem cardinal.to_part_enat_apply_of_aleph_0_le {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
⇑cardinal.to_part_enat c = ⊤
source
@[simp]
theorem cardinal.to_part_enat_cast (n : ℕ) :
⇑cardinal.to_part_enat ↑n = ↑n
source
@[simp]
theorem cardinal.mk_to_part_enat_of_infinite {α : Type u} [h : infinite α] :
⇑cardinal.to_part_enat (cardinal.mk α) = ⊤
source
@[simp]
theorem cardinal.aleph_0_to_part_enat  :
⇑cardinal.to_part_enat cardinal.aleph_0 = ⊤
source
theorem cardinal.to_part_enat_eq_top_iff_le_aleph_0 {c : cardinal} :
⇑cardinal.to_part_enat c = ⊤ ↔ cardinal.aleph_0 ≤ c
source
theorem cardinal.to_part_enat_le_iff_le_of_le_aleph_0 {c c' : cardinal} (h : c ≤ cardinal.aleph_0) :
⇑cardinal.to_part_enat c ≤ ⇑cardinal.to_part_enat c' ↔ c ≤ c'
source
theorem cardinal.to_part_enat_le_iff_le_of_lt_aleph_0 {c c' : cardinal} (hc' : c' < cardinal.aleph_0) :
⇑cardinal.to_part_enat c ≤ ⇑cardinal.to_part_enat c' ↔ c ≤ c'
source
theorem cardinal.to_part_enat_eq_iff_eq_of_le_aleph_0 {c c' : cardinal} (hc : c ≤ cardinal.aleph_0) (hc' : c' ≤ cardinal.aleph_0) :
⇑cardinal.to_part_enat c = ⇑cardinal.to_part_enat c' ↔ c = c'
source
theorem cardinal.to_part_enat_mono {c c' : cardinal} (h : c ≤ c') :
⇑cardinal.to_part_enat c ≤ ⇑cardinal.to_part_enat c'
source
theorem cardinal.to_part_enat_surjective  :
function.surjective ⇑cardinal.to_part_enat
source
theorem cardinal.to_part_enat_lift (c : cardinal) :
⇑cardinal.to_part_enat c.lift = ⇑cardinal.to_part_enat c
source
theorem cardinal.to_part_enat_congr {α : Type u} {β : Type v} (e : α ≃ β) :
⇑cardinal.to_part_enat (cardinal.mk α) = ⇑cardinal.to_part_enat (cardinal.mk β)
source
theorem cardinal.mk_to_part_enat_eq_coe_card {α : Type u} [fintype α] :
⇑cardinal.to_part_enat (cardinal.mk α) = ↑(fintype.card α)
source
theorem cardinal.mk_int  :
cardinal.mk ℤ = cardinal.aleph_0
source
theorem cardinal.mk_pnat  :
cardinal.mk ℕ+ = cardinal.aleph_0
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  :
cardinal.mk empty = 0
source
@[simp]
theorem cardinal.mk_pempty  :
cardinal.mk pempty = 0
source
@[simp]
theorem cardinal.mk_punit  :
cardinal.mk punit = 1
source
theorem cardinal.mk_unit  :
cardinal.mk unit = 1
source
@[simp]
theorem cardinal.mk_singleton {α : Type u} (x : α) :
cardinal.mk ↥{x} = 1
source
@[simp]
theorem cardinal.mk_plift_true  :
cardinal.mk (plift true) = 1
source
@[simp]
theorem cardinal.mk_plift_false  :
cardinal.mk (plift false) = 0
source
@[simp]
theorem cardinal.mk_vector (α : Type u) (n : ℕ) :
cardinal.mk (vector α n) = cardinal.mk α ^ n
source
theorem cardinal.mk_list_eq_sum_pow (α : Type u) :
cardinal.mk (list α) = cardinal.sum (λ (n : ℕ), cardinal.mk α ^ n)
source
theorem cardinal.mk_quot_le {α : Type u} {r : α → α → Prop} :
cardinal.mk (quot r) ≤ cardinal.mk α
source
theorem cardinal.mk_quotient_le {α : Type u} {s : setoid α} :
cardinal.mk (quotient s) ≤ cardinal.mk α
source
theorem cardinal.mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x : α⦄, p x → q x) :
cardinal.mk (subtype p) ≤ cardinal.mk (subtype q)
source
@[simp]
theorem cardinal.mk_emptyc (α : Type u) :
cardinal.mk ↥∅ = 0
source
theorem cardinal.mk_emptyc_iff {α : Type u} {s : set α} :
cardinal.mk ↥s = 0 ↔ s = ∅
source
@[simp]
theorem cardinal.mk_univ {α : Type u} :
cardinal.mk ↥set.univ = cardinal.mk α
source
theorem cardinal.mk_image_le {α β : Type u} {f : α → β} {s : set α} :
cardinal.mk ↥(f '' s) ≤ cardinal.mk ↥s
source
theorem cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(cardinal.mk ↥(f '' s)).lift ≤ (cardinal.mk ↥s).lift
source
theorem cardinal.mk_range_le {α β : Type u} {f : α → β} :
cardinal.mk ↥(set.range f) ≤ cardinal.mk α
source
theorem cardinal.mk_range_le_lift {α : Type u} {β : Type v} {f : α → β} :
(cardinal.mk ↥(set.range f)).lift ≤ (cardinal.mk α).lift
source
theorem cardinal.mk_range_eq {α β : Type u} (f : α → β) (h : function.injective f) :
cardinal.mk ↥(set.range f) = cardinal.mk α
source
theorem cardinal.mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
(cardinal.mk ↥(set.range f)).lift = (cardinal.mk α).lift
source
theorem cardinal.mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) :
(cardinal.mk ↥(set.range f)).lift = (cardinal.mk α).lift
source
theorem cardinal.mk_image_eq {α β : Type u} {f : α → β} {s : set α} (hf : function.injective f) :
cardinal.mk ↥(f '' s) = cardinal.mk ↥s
source
theorem cardinal.mk_Union_le_sum_mk {α ι : Type u} {f : ι → set α} :
cardinal.mk (↥⋃ (i : ι), f i) ≤ cardinal.sum (λ (i : ι), cardinal.mk ↥(f i))
source
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))
source
theorem cardinal.mk_Union_le {α ι : Type u} (f : ι → set α) :
cardinal.mk (↥⋃ (i : ι), f i) ≤ cardinal.mk ι * ⨆ (i : ι), cardinal.mk ↥(f i)
source
theorem cardinal.mk_sUnion_le {α : Type u} (A : set (set α)) :
cardinal.mk (↥⋃₀ A) ≤ cardinal.mk ↥A * ⨆ (s : ↥A), cardinal.mk ↥s
source
theorem cardinal.mk_bUnion_le {ι α : Type u} (A : ι → set α) (s : set ι) :
cardinal.mk (↥⋃ (x : ι) (H : x ∈ s), A x) ≤ cardinal.mk ↥s * ⨆ (x : ↥s), cardinal.mk ↥(A x.val)
source
theorem cardinal.finset_card_lt_aleph_0 {α : Type u} (s : finset α) :
cardinal.mk ↥↑s < cardinal.aleph_0
source
theorem cardinal.mk_set_eq_nat_iff_finset {α : Type u_1} {s : set α} {n : ℕ} :
cardinal.mk ↥s = ↑n ↔ ∃ (t : finset α), ↑t = s ∧ t.card = n
source
theorem cardinal.mk_eq_nat_iff_finset {α : Type u} {n : ℕ} :
cardinal.mk α = ↑n ↔ ∃ (t : finset α), ↑t = set.univ ∧ t.card = n
source
theorem cardinal.mk_eq_nat_iff_fintype {α : Type u} {n : ℕ} :
cardinal.mk α = ↑n ↔ ∃ (h : fintype α), fintype.card α = n
source
theorem cardinal.mk_union_add_mk_inter {α : Type u} {S T : set α} :
cardinal.mk ↥(S ∪ T) + cardinal.mk ↥(S ∩ T) = cardinal.mk ↥S + cardinal.mk ↥T
source
theorem cardinal.mk_union_le {α : Type u} (S T : set α) :
cardinal.mk ↥(S ∪ T) ≤ cardinal.mk ↥S + cardinal.mk ↥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) :
cardinal.mk ↥(S ∪ T) = cardinal.mk ↥S + cardinal.mk ↥T
source
theorem cardinal.mk_insert {α : Type u} {s : set α} {a : α} (h : a ∉ s) :
cardinal.mk ↥(has_insert.insert a s) = cardinal.mk ↥s + 1
source
theorem cardinal.mk_sum_compl {α : Type u_1} (s : set α) :
cardinal.mk ↥s + cardinal.mk ↥sᶜ = cardinal.mk α
source
theorem cardinal.mk_le_mk_of_subset {α : Type u_1} {s t : set α} (h : s ⊆ t) :
cardinal.mk ↥s ≤ cardinal.mk ↥t
source
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}
source
theorem cardinal.le_mk_diff_add_mk {α : Type u} (S T : set α) :
cardinal.mk ↥S ≤ cardinal.mk ↥(S \ T) + cardinal.mk ↥T
source
theorem cardinal.mk_diff_add_mk {α : Type u} {S T : set α} (h : T ⊆ S) :
cardinal.mk ↥(S \ T) + cardinal.mk ↥T = cardinal.mk ↥S
source
theorem cardinal.mk_union_le_aleph_0 {α : Type u_1} {P Q : set α} :
cardinal.mk ↥(P ∪ Q) ≤ cardinal.aleph_0 ↔ cardinal.mk ↥P ≤ cardinal.aleph_0 ∧ cardinal.mk ↥Q ≤ cardinal.aleph_0
source
theorem cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : α → β) (s : set α) (h : function.injective f) :
(cardinal.mk ↥(f '' s)).lift = (cardinal.mk ↥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) :
(cardinal.mk ↥(f '' s)).lift = (cardinal.mk ↥s).lift
source
theorem cardinal.mk_image_eq_of_inj_on {α β : Type u} (f : α → β) (s : set α) (h : set.inj_on f s) :
cardinal.mk ↥(f '' s) = cardinal.mk ↥s
source
theorem cardinal.mk_subtype_of_equiv {α β : Type u} (p : β → Prop) (e : α ≃ β) :
cardinal.mk {a // p (⇑e a)} = cardinal.mk {b // p b}
source
theorem cardinal.mk_sep {α : Type u} (s : set α) (t : α → Prop) :
cardinal.mk ↥{x ∈ s | t x} = cardinal.mk ↥{x : ↥s | t x.val}
source
theorem cardinal.mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : set β) (h : function.injective f) :
(cardinal.mk ↥(f ⁻¹' s)).lift ≤ (cardinal.mk ↥s).lift
source
theorem cardinal.mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : set β) (h : s ⊆ set.range f) :
(cardinal.mk ↥s).lift ≤ (cardinal.mk ↥(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) :
(cardinal.mk ↥(f ⁻¹' s)).lift = (cardinal.mk ↥s).lift
source
theorem cardinal.mk_preimage_of_injective {α β : Type u} (f : α → β) (s : set β) (h : function.injective f) :
cardinal.mk ↥(f ⁻¹' s) ≤ cardinal.mk ↥s
source
theorem cardinal.mk_preimage_of_subset_range {α β : Type u} (f : α → β) (s : set β) (h : s ⊆ set.range f) :
cardinal.mk ↥s ≤ cardinal.mk ↥(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) :
cardinal.mk ↥(f ⁻¹' s) = cardinal.mk ↥s
source
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
source
theorem cardinal.mk_subset_ge_of_subset_image {α β : Type u} (f : α → β) {s : set α} {t : set β} (h : t ⊆ f '' s) :
cardinal.mk ↥t ≤ cardinal.mk ↥{x ∈ s | f x ∈ t}
source
theorem cardinal.le_mk_iff_exists_subset {c : cardinal} {α : Type u} {s : set α} :
c ≤ cardinal.mk ↥s ↔ ∃ (p : set α), p ⊆ s ∧ cardinal.mk ↥p = c
source
theorem cardinal.two_le_iff {α : Type u} :
2 ≤ cardinal.mk α ↔ ∃ (x y : α), x ≠ y
source
theorem cardinal.two_le_iff' {α : Type u} (x : α) :
2 ≤ cardinal.mk α ↔ ∃ (y : α), y ≠ x
source
theorem cardinal.mk_eq_two_iff {α : Type u} :
cardinal.mk α = 2 ↔ ∃ (x y : α), x ≠ y ∧ {x, y} = set.univ
source
theorem cardinal.mk_eq_two_iff' {α : Type u} (x : α) :
cardinal.mk α = 2 ↔ ∃! (y : α), y ≠ x
source
theorem cardinal.exists_not_mem_of_length_lt {α : Type u_1} (l : list α) (h : ↑(l.length) < cardinal.mk α) :
∃ (z : α), z ∉ l
source
theorem cardinal.three_le {α : Type u_1} (h : 3 ≤ cardinal.mk α) (x y : α) :
∃ (z : α), z ≠ x ∧ z ≠ y
source
noncomputable def cardinal.powerlt (a b : cardinal) :
cardinal

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

Equations
source
theorem cardinal.le_powerlt {b c : cardinal} (a : cardinal) (h : c < b) :
a ^ c ≤ a ^< b
source
theorem cardinal.powerlt_le {a b c : cardinal} :
a ^< b ≤ c ↔ ∀ (x : cardinal), x < b → a ^ x ≤ c
source
theorem cardinal.powerlt_le_powerlt_left {a b c : cardinal} (h : b ≤ c) :
a ^< b ≤ a ^< c
source
theorem cardinal.powerlt_mono_left (a : cardinal) :
monotone (λ (c : cardinal), a ^< c)
source
theorem cardinal.powerlt_succ {a b : cardinal} (h : a ≠ 0) :
a ^< order.succ b = a ^ b
source
theorem cardinal.powerlt_min {a b c : cardinal} :
a ^< linear_order.min b c = linear_order.min (a ^< b) (a ^< c)
source
theorem cardinal.powerlt_max {a b c : cardinal} :
a ^< linear_order.max b c = linear_order.max (a ^< b) (a ^< c)
source
theorem cardinal.zero_powerlt {a : cardinal} (h : a ≠ 0) :
0 ^< a = 1
source
@[simp]
theorem cardinal.powerlt_zero {a : cardinal} :
a ^< 0 = 0
source
meta def tactic.positivity_cardinal_pow  :
expr → tactic tactic.positivity.strictness

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