Documentation

Mathlib.SetTheory.Cardinal.Basic

Basic results on cardinal numbers #

We provide a collection of basic results on cardinal numbers, in particular focusing on finite/countable/small types and sets.

Main definitions #

Cardinal.powerlt a b or a ^< b is defined as the supremum of a ^ c for c < b.

References #

https://en.wikipedia.org/wiki/Cardinal_number

Tags #

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

Lifting cardinals to a higher universe #

@[simp]

theorem Cardinal.mk_preimage_down {α : Type u} {s : Set α} :

mk ↑(ULift.down ⁻¹' s) = lift.{v, u} (mk ↑s)

theorem Cardinal.lift_mk_shrink (α : Type u) [Small.{v, u} α] :

lift.{max u w, v} (mk (Shrink.{v, u} α)) = lift.{max v w, u} (mk α)

@[simp]

theorem Cardinal.lift_mk_shrink' (α : Type u) [Small.{v, u} α] :

lift.{u, v} (mk (Shrink.{v, u} α)) = lift.{v, u} (mk α)

@[simp]

theorem Cardinal.lift_mk_shrink'' (α : Type (max u v)) [Small.{v, max u v} α] :

lift.{u, v} (mk (Shrink.{v, max u v} α)) = mk α

theorem Cardinal.prod_eq_of_fintype {α : Type u} [h : Fintype α] (f : α → Cardinal.{v}) :

prod f = lift.{u, v} (∏ i : α, f i)

Basic cardinals #

theorem Cardinal.le_one_iff_subsingleton {α : Type u} :

mk α ≤ 1 ↔ Subsingleton α

@[simp]

theorem Cardinal.mk_le_one_iff_set_subsingleton {α : Type u} {s : Set α} :

mk ↑s ≤ 1 ↔ s.Subsingleton

theorem Set.Subsingleton.cardinalMk_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.

Order properties #

theorem Cardinal.one_lt_iff_nontrivial {α : Type u} :

1 < mk α ↔ Nontrivial α

theorem Cardinal.sInf_eq_zero_iff {s : Set Cardinal.{u_1}} :

sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

theorem Cardinal.iInf_eq_zero_iff {ι : Sort u_1} {f : ι → Cardinal.{u_2}} :

⨅ (i : ι), f i = 0 ↔ IsEmpty ι ∨ ∃ (i : ι), f i = 0

theorem Cardinal.iSup_of_empty {ι : Sort u_1} (f : ι → Cardinal.{u_2}) [IsEmpty ι] :

iSup f = 0

A variant of ciSup_of_empty but with 0 on the RHS for convenience

@[simp]

theorem Cardinal.lift_sInf (s : Set Cardinal.{v}) :

lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

@[simp]

theorem Cardinal.lift_iInf {ι : Sort u_1} (f : ι → Cardinal.{v}) :

lift.{u, v} (iInf f) = ⨅ (i : ι), lift.{u, v} (f i)

Small sets of cardinals #

instance Cardinal.small_Iic (a : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Iic a)

instance Cardinal.small_Iio (a : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Iio a)

instance Cardinal.small_Icc (a b : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Icc a b)

instance Cardinal.small_Ico (a b : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Ico a b)

instance Cardinal.small_Ioc (a b : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Ioc a b)

instance Cardinal.small_Ioo (a b : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Ioo a b)

theorem Cardinal.bddAbove_iff_small {s : Set Cardinal.{u}} :

BddAbove s ↔ Small.{u, u + 1} ↑s

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

theorem Cardinal.bddAbove_of_small (s : Set Cardinal.{u}) [h : Small.{u, u + 1} ↑s] :

theorem Cardinal.bddAbove_range {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Cardinal.{u}) :

BddAbove (Set.range f)

theorem Cardinal.bddAbove_image (f : Cardinal.{u} → Cardinal.{max u v}) {s : Set Cardinal.{u}} (hs : BddAbove s) :

BddAbove (f '' s)

theorem Cardinal.bddAbove_range_comp {ι : Type u} {f : ι → Cardinal.{v}} (hf : BddAbove (Set.range f)) (g : Cardinal.{v} → Cardinal.{max v w}) :

BddAbove (Set.range (g ∘ f))

theorem not_small_cardinal :

¬Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}

The type of cardinals in universe u is not Small.{u}. This is a version of the Burali-Forti paradox.

instance Cardinal.uncountable :

Uncountable Cardinal.{u}

Bounds on suprema #

theorem Cardinal.sum_le_lift_mk_mul_iSup_lift {ι : Type u} (f : ι → Cardinal.{v}) :

sum f ≤ lift.{v, u} (mk ι) * ⨆ (i : ι), lift.{u, v} (f i)

theorem Cardinal.sum_le_lift_mk_mul_iSup {ι : Type u} (f : ι → Cardinal.{max u v}) :

sum f ≤ lift.{v, u} (mk ι) * ⨆ (i : ι), f i

theorem Cardinal.sum_le_mk_mul_iSup {ι : Type u} (f : ι → Cardinal.{u}) :

sum f ≤ mk ι * ⨆ (i : ι), f i

@[deprecated Cardinal.sum_le_lift_mk_mul_iSup (since := "2025-09-04")]

theorem Cardinal.sum_le_iSup_lift {ι : Type u} (f : ι → Cardinal.{max u v}) :

sum f ≤ lift.{v, u} (mk ι) * ⨆ (i : ι), f i

Alias of Cardinal.sum_le_lift_mk_mul_iSup.

@[deprecated Cardinal.sum_le_mk_mul_iSup (since := "2025-09-04")]

theorem Cardinal.sum_le_iSup {ι : Type u} (f : ι → Cardinal.{u}) :

sum f ≤ mk ι * ⨆ (i : ι), f i

Alias of Cardinal.sum_le_mk_mul_iSup.

theorem Cardinal.lift_sSup {s : Set Cardinal.{u_1}} (hs : BddAbove s) :

lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)

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

theorem Cardinal.lift_iSup {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (Set.range f)) :

lift.{u, w} (iSup f) = ⨆ (i : ι), lift.{u, w} (f i)

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

theorem Cardinal.lift_iSup_le {ι : Type v} {f : ι → Cardinal.{w}} {t : Cardinal.{max u w}} (hf : BddAbove (Set.range f)) (w : ∀ (i : ι), lift.{u, w} (f i) ≤ t) :

lift.{u, w} (iSup f) ≤ 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_iSup_le_iff {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (Set.range f)) {t : Cardinal.{max u w}} :

lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

theorem Cardinal.lift_iSup_le_lift_iSup {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{w}} {f' : ι' → Cardinal.{w'}} (hf : BddAbove (Set.range f)) (hf' : BddAbove (Set.range f')) {g : ι → ι'} (h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))) :

lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')

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_iSup_le_lift_iSup' {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{v}} {f' : ι' → Cardinal.{v'}} (hf : BddAbove (Set.range f)) (hf' : BddAbove (Set.range f')) (g : ι → ι') (h : ∀ (i : ι), lift.{v', v} (f i) ≤ lift.{v, v'} (f' (g i))) :

lift.{v', v} (iSup f) ≤ lift.{v, v'} (iSup f')

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

theorem Cardinal.lift_iSup_le_sum {ι : Type u} [Small.{v, u} ι] (f : ι → Cardinal.{v}) :

lift.{u, v} (⨆ (i : ι), f i) ≤ sum f

Properties about the cast from `ℕ` #

theorem Cardinal.mk_finset_of_fintype {α : Type u} [Fintype α] :

mk (Finset α) = 2 ^ Fintype.card α

theorem Cardinal.nat_succ (n : ℕ) :

↑n.succ = Order.succ ↑n

theorem Cardinal.succ_natCast (n : ℕ) :

Order.succ ↑n = ↑n + 1

theorem Cardinal.natCast_add_one_le_iff {n : ℕ} {c : Cardinal.{u_1}} :

↑n + 1 ≤ c ↔ ↑n < c

theorem Cardinal.two_le_iff_one_lt {c : Cardinal.{u_1}} :

2 ≤ c ↔ 1 < c

@[simp]

theorem Cardinal.succ_zero :

Order.succ 0 = 1

theorem Cardinal.one_lt_two :

1 < 2

theorem Cardinal.exists_finset_eq_card {α : Type u_1} {n : ℕ} (h : ↑n ≤ mk α) :

∃ (s : Finset α), n = s.card

theorem Cardinal.exists_finset_le_card (α : Type u_1) (n : ℕ) (h : ↑n ≤ mk α) :

∃ (s : Finset α), n ≤ s.card

theorem Cardinal.card_le_of {α : Type u} {n : ℕ} (H : ∀ (s : Finset α), s.card ≤ n) :

mk α ≤ ↑n

theorem Cardinal.cantor' (a : Cardinal.{u_1}) {b : Cardinal.{u_1}} (hb : 1 < b) :

a < b ^ a

theorem Cardinal.one_le_iff_pos {c : Cardinal.{u_1}} :

1 ≤ c ↔ 0 < c

theorem Cardinal.one_le_iff_ne_zero {c : Cardinal.{u_1}} :

1 ≤ c ↔ c ≠ 0

@[simp]

theorem Cardinal.lt_one_iff_zero {c : Cardinal.{u_1}} :

c < 1 ↔ c = 0

theorem Cardinal.le_one_iff {c : Cardinal.{u_1}} :

c ≤ 1 ↔ c = 0 ∨ c = 1

Properties about `aleph0` #

@[simp]

theorem Cardinal.natCast_lt_aleph0 {n : ℕ} :

@[deprecated Cardinal.natCast_lt_aleph0 (since := "2026-01-21")]

theorem Cardinal.nat_lt_aleph0 (n : ℕ) :

@[simp]

theorem Cardinal.natCast_le_aleph0 {n : ℕ} :

↑n ≤ aleph0

@[simp]

theorem Cardinal.ofNat_lt_aleph0 {n : ℕ} [n.AtLeastTwo] :

OfNat.ofNat n < aleph0

@[simp]

theorem Cardinal.ofNat_le_aleph0 {n : ℕ} [n.AtLeastTwo] :

OfNat.ofNat n ≤ aleph0

@[simp]

theorem Cardinal.one_lt_aleph0 :

@[simp]

theorem Cardinal.one_le_aleph0 :

theorem Cardinal.lt_aleph0 {c : Cardinal.{u_1}} :

c < aleph0 ↔ ∃ (n : ℕ), c = ↑n

theorem Cardinal.succ_eq_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < aleph0) :

Order.succ c = c + 1

theorem Cardinal.aleph0_le {c : Cardinal.{u_1}} :

aleph0 ≤ c ↔ ∀ (n : ℕ), ↑n ≤ c

theorem Cardinal.isSuccPrelimit_aleph0 :

Order.IsSuccPrelimit aleph0

theorem Cardinal.isSuccLimit_aleph0 :

Order.IsSuccLimit aleph0

theorem Cardinal.not_isSuccLimit_natCast (n : ℕ) :

¬Order.IsSuccLimit ↑n

theorem Cardinal.not_isSuccLimit_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < aleph0) :

¬Order.IsSuccLimit c

theorem Cardinal.aleph0_le_of_isSuccLimit {c : Cardinal.{u_1}} (h : Order.IsSuccLimit c) :

theorem Cardinal.isStrongLimit_aleph0 :

aleph0.IsStrongLimit

theorem Cardinal.IsStrongLimit.aleph0_le {c : Cardinal.{u_1}} (H : c.IsStrongLimit) :

theorem Cardinal.exists_eq_natCast_of_iSup_eq {ι : Type u} [Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (Set.range f)) (n : ℕ) (h : ⨆ (i : ι), f i = ↑n) :

∃ (i : ι), f i = ↑n

@[simp]

theorem Cardinal.range_natCast :

Set.range Nat.cast = Set.Iio aleph0

theorem Cardinal.mk_eq_nat_iff {α : Type u} {n : ℕ} :

mk α = ↑n ↔ Nonempty (α ≃ Fin n)

theorem Cardinal.lt_aleph0_iff_finite {α : Type u} :

mk α < aleph0 ↔ Finite α

theorem Cardinal.lt_aleph0_iff_fintype {α : Type u} :

mk α < aleph0 ↔ Nonempty (Fintype α)

theorem Cardinal.lt_aleph0_of_finite (α : Type u) [Finite α] :

theorem Cardinal.lt_aleph0_iff_set_finite {α : Type u} {S : Set α} :

mk ↑S < aleph0 ↔ S.Finite

theorem Set.Finite.lt_aleph0 {α : Type u} {S : Set α} :

S.Finite → Cardinal.mk ↑S < Cardinal.aleph0

Alias of the reverse direction of Cardinal.lt_aleph0_iff_set_finite.

@[simp]

theorem Cardinal.lt_aleph0_iff_subtype_finite {α : Type u} {p : α → Prop} :

mk { x : α // p x } < aleph0 ↔ {x : α | p x}.Finite

theorem Cardinal.mk_le_aleph0_iff {α : Type u} :

mk α ≤ aleph0 ↔ Countable α

@[simp]

theorem Cardinal.mk_le_aleph0 {α : Type u} [Countable α] :

mk α ≤ aleph0

theorem Cardinal.le_aleph0_iff_set_countable {α : Type u} {s : Set α} :

mk ↑s ≤ aleph0 ↔ s.Countable

theorem Set.Countable.le_aleph0 {α : Type u} {s : Set α} :

s.Countable → Cardinal.mk ↑s ≤ Cardinal.aleph0

Alias of the reverse direction of Cardinal.le_aleph0_iff_set_countable.

@[simp]

theorem Cardinal.le_aleph0_iff_subtype_countable {α : Type u} {p : α → Prop} :

mk { x : α // p x } ≤ aleph0 ↔ {x : α | p x}.Countable

theorem Cardinal.aleph0_lt_mk_iff {α : Type u} :

aleph0 < mk α ↔ Uncountable α

@[simp]

theorem Cardinal.aleph0_lt_mk {α : Type u} [Uncountable α] :

instance Cardinal.canLiftCardinalNat :

CanLift Cardinal.{u_1} ℕ Nat.cast fun (x : Cardinal.{u_1}) => x < aleph0

theorem Cardinal.add_lt_aleph0 {a b : Cardinal.{u_1}} (ha : a < aleph0) (hb : b < aleph0) :

theorem Cardinal.add_lt_aleph0_iff {a b : Cardinal.{u_1}} :

a + b < aleph0 ↔ a < aleph0 ∧ b < aleph0

theorem Cardinal.aleph0_le_add_iff {a b : Cardinal.{u_1}} :

aleph0 ≤ a + b ↔ aleph0 ≤ a ∨ aleph0 ≤ b

theorem Cardinal.nsmul_lt_aleph0_iff {a : Cardinal.{u_1}} {n : ℕ} :

n • a < aleph0 ↔ n = 0 ∨ a < aleph0

See also Cardinal.nsmul_lt_aleph0_iff_of_ne_zero if you already have n ≠ 0.

theorem Cardinal.nsmul_lt_aleph0_iff_of_ne_zero {n : ℕ} {a : Cardinal.{u_1}} (h : n ≠ 0) :

n • a < aleph0 ↔ a < aleph0

See also Cardinal.nsmul_lt_aleph0_iff for a hypothesis-free version.

theorem Cardinal.mul_lt_aleph0 {a b : Cardinal.{u_1}} (ha : a < aleph0) (hb : b < aleph0) :

theorem Cardinal.mul_lt_aleph0_iff {a b : Cardinal.{u_1}} :

a * b < aleph0 ↔ a = 0 ∨ b = 0 ∨ a < aleph0 ∧ b < aleph0

theorem Cardinal.aleph0_le_mul_iff {a b : Cardinal.{u_1}} :

aleph0 ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (aleph0 ≤ a ∨ aleph0 ≤ b)

See also Cardinal.aleph0_le_mul_iff.

theorem Cardinal.aleph0_le_mul_iff' {a b : Cardinal.{u}} :

aleph0 ≤ a * b ↔ a ≠ 0 ∧ aleph0 ≤ b ∨ aleph0 ≤ a ∧ b ≠ 0

See also Cardinal.aleph0_le_mul_iff'.

theorem Cardinal.mul_lt_aleph0_iff_of_ne_zero {a b : Cardinal.{u_1}} (ha : a ≠ 0) (hb : b ≠ 0) :

a * b < aleph0 ↔ a < aleph0 ∧ b < aleph0

theorem Cardinal.power_lt_aleph0 {a b : Cardinal.{u_1}} (ha : a < aleph0) (hb : b < aleph0) :

theorem Cardinal.eq_one_iff_unique {α : Type u_1} :

mk α = 1 ↔ Subsingleton α ∧ Nonempty α

theorem Cardinal.infinite_iff {α : Type u} :

Infinite α ↔ aleph0 ≤ mk α

theorem Cardinal.aleph0_le_mk_iff {α : Type u} :

aleph0 ≤ mk α ↔ Infinite α

theorem Cardinal.mk_lt_aleph0_iff {α : Type u} :

mk α < aleph0 ↔ Finite α

@[simp]

theorem Cardinal.mk_lt_aleph0 {α : Type u} [Finite α] :

@[simp]

theorem Cardinal.aleph0_le_mk (α : Type u) [Infinite α] :

aleph0 ≤ mk α

theorem Infinite.of_cardinalMk_le {α β : Type u} [Infinite α] (h : Cardinal.mk α ≤ Cardinal.mk β) :

@[simp]

theorem Cardinal.mk_eq_aleph0 (α : Type u_1) [Countable α] [Infinite α] :

theorem Cardinal.denumerable_iff {α : Type u} :

Nonempty (Denumerable α) ↔ mk α = aleph0

theorem Cardinal.mk_denumerable (α : Type u) [Denumerable α] :

theorem Set.countable_infinite_iff_nonempty_denumerable {α : Type u_1} {s : Set α} :

s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable ↑s)

@[simp]

theorem Cardinal.aleph0_add_aleph0 :

aleph0 + aleph0 = aleph0

theorem Cardinal.aleph0_mul_aleph0 :

aleph0 * aleph0 = aleph0

@[simp]

theorem Cardinal.nat_mul_aleph0 {n : ℕ} (hn : n ≠ 0) :

↑n * aleph0 = aleph0

@[simp]

theorem Cardinal.aleph0_mul_nat {n : ℕ} (hn : n ≠ 0) :

aleph0 * ↑n = aleph0

@[simp]

theorem Cardinal.ofNat_mul_aleph0 {n : ℕ} [n.AtLeastTwo] :

OfNat.ofNat n * aleph0 = aleph0

@[simp]

theorem Cardinal.aleph0_mul_ofNat {n : ℕ} [n.AtLeastTwo] :

aleph0 * OfNat.ofNat n = aleph0

@[simp]

theorem Cardinal.add_le_aleph0 {c₁ c₂ : Cardinal.{u_1}} :

c₁ + c₂ ≤ aleph0 ↔ c₁ ≤ aleph0 ∧ c₂ ≤ aleph0

@[simp]

theorem Cardinal.aleph0_add_nat (n : ℕ) :

aleph0 + ↑n = aleph0

@[simp]

theorem Cardinal.nat_add_aleph0 (n : ℕ) :

↑n + aleph0 = aleph0

@[simp]

theorem Cardinal.ofNat_add_aleph0 {n : ℕ} [n.AtLeastTwo] :

OfNat.ofNat n + aleph0 = aleph0

@[simp]

theorem Cardinal.aleph0_add_ofNat {n : ℕ} [n.AtLeastTwo] :

aleph0 + OfNat.ofNat n = aleph0

theorem Cardinal.exists_nat_eq_of_le_nat {c : Cardinal.{u_1}} {n : ℕ} (h : c ≤ ↑n) :

∃ m ≤ n, c = ↑m

theorem Cardinal.mk_int :

mk ℤ = aleph0

theorem Cardinal.mk_pnat :

mk ℕ+ = aleph0

Cardinalities of basic sets and types #

@[simp]

theorem Cardinal.mk_additive {α : Type u} :

mk (Additive α) = mk α

@[simp]

theorem Cardinal.mk_multiplicative {α : Type u} :

mk (Multiplicative α) = mk α

@[simp]

theorem Cardinal.mk_mulOpposite {α : Type u} :

mk αᵐᵒᵖ = mk α

@[simp]

theorem Cardinal.mk_addOpposite {α : Type u} :

mk αᵃᵒᵖ = mk α

theorem Cardinal.mk_singleton {α : Type u} (x : α) :

mk ↑{x} = 1

@[simp]

theorem Cardinal.mk_vector (α : Type u) (n : ℕ) :

mk (List.Vector α n) = mk α ^ n

theorem Cardinal.mk_list_eq_sum_pow (α : Type u) :

mk (List α) = sum fun (n : ℕ) => mk α ^ n

theorem Cardinal.sum_zero_pow :

(sum fun (n : ℕ) => 0 ^ n) = 1

theorem Cardinal.mk_quot_le {α : Type u} {r : α → α → Prop} :

mk (Quot r) ≤ mk α

theorem Cardinal.mk_quotient_le {α : Type u} {s : Setoid α} :

mk (Quotient s) ≤ mk α

theorem Cardinal.mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x : α⦄, p x → q x) :

mk (Subtype p) ≤ mk (Subtype q)

theorem Cardinal.mk_le_mk_of_subset {α : Type u_1} {s t : Set α} (h : s ⊆ t) :

mk ↑s ≤ mk ↑t

theorem Cardinal.mk_monotone {α : Type u} :

Monotone (mk ∘ Set.Elem)

@[deprecated Cardinal.mk_eq_zero (since := "2026-01-31")]

theorem Cardinal.mk_emptyCollection (α : Type u) :

mk ↑∅ = 0

theorem Cardinal.mk_set_eq_zero_iff {α : Type u} {s : Set α} :

mk ↑s = 0 ↔ s = ∅

@[deprecated Cardinal.mk_set_eq_zero_iff (since := "2026-01-31")]

theorem Cardinal.mk_emptyCollection_iff {α : Type u} {s : Set α} :

mk ↑s = 0 ↔ s = ∅

Alias of Cardinal.mk_set_eq_zero_iff.

theorem Cardinal.mk_set_ne_zero_iff {α : Type u} {s : Set α} :

mk ↑s ≠ 0 ↔ s.Nonempty

@[simp]

theorem Cardinal.mk_univ {α : Type u} :

mk ↑Set.univ = mk α

@[simp]

theorem Cardinal.mk_setProd {α β : Type u} (s : Set α) (t : Set β) :

mk ↑(s ×ˢ t) = mk ↑s * mk ↑t

theorem Cardinal.mk_image_le {α β : Type u} {f : α → β} {s : Set α} :

mk ↑(f '' s) ≤ mk ↑s

theorem Cardinal.mk_image2_le {α β γ : Type u} {f : α → β → γ} {s : Set α} {t : Set β} :

mk ↑(Set.image2 f s t) ≤ mk ↑s * mk ↑t

theorem Cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : Set α} :

lift.{u, v} (mk ↑(f '' s)) ≤ lift.{v, u} (mk ↑s)

theorem Cardinal.mk_range_le {α β : Type u} {f : α → β} :

mk ↑(Set.range f) ≤ mk α

theorem Cardinal.mk_range_le_lift {α : Type u} {β : Type v} {f : α → β} :

lift.{u, v} (mk ↑(Set.range f)) ≤ lift.{v, u} (mk α)

theorem Cardinal.mk_range_eq {α β : Type u} (f : α → β) (h : Function.Injective f) :

mk ↑(Set.range f) = mk α

theorem Cardinal.mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) :

lift.{u, v} (mk ↑(Set.range f)) = lift.{v, u} (mk α)

@[deprecated Cardinal.mk_range_eq_of_injective (since := "2026-01-06")]

theorem Cardinal.mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) :

lift.{max u w, v} (mk ↑(Set.range f)) = lift.{max v w, u} (mk α)

theorem Cardinal.lift_mk_le_lift_mk_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) :

lift.{v, u} (mk α) ≤ lift.{u, v} (mk β)

theorem Cardinal.lift_mk_le_lift_mk_of_surjective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Surjective f) :

lift.{u, v} (mk β) ≤ lift.{v, u} (mk α)

theorem Cardinal.mk_image_eq_of_injOn {α β : Type u} (f : α → β) (s : Set α) (h : Set.InjOn f s) :

mk ↑(f '' s) = mk ↑s

theorem Cardinal.mk_image_eq_of_injOn_lift {α : Type u} {β : Type v} (f : α → β) (s : Set α) (h : Set.InjOn f s) :

lift.{u, v} (mk ↑(f '' s)) = lift.{v, u} (mk ↑s)

theorem Cardinal.mk_image_eq {α β : Type u} {f : α → β} {s : Set α} (hf : Function.Injective f) :

mk ↑(f '' s) = mk ↑s

theorem Cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : α → β) (s : Set α) (h : Function.Injective f) :

lift.{u, v} (mk ↑(f '' s)) = lift.{v, u} (mk ↑s)

@[simp]

theorem Cardinal.mk_image_embedding_lift {α : Type u} {β : Type v} (f : α ↪ β) (s : Set α) :

lift.{u, v} (mk ↑(⇑f '' s)) = lift.{v, u} (mk ↑s)

@[simp]

theorem Cardinal.mk_image_embedding {α β : Type u} (f : α ↪ β) (s : Set α) :

mk ↑(⇑f '' s) = mk ↑s

theorem Cardinal.iSup_mk_le_mk_iUnion {α : Type u} {ι : Type v} {f : ι → Set α} :

⨆ (i : ι), mk ↑(f i) ≤ mk ↑(⋃ (i : ι), f i)

theorem Cardinal.mk_iUnion_le_sum_mk {α ι : Type u} {f : ι → Set α} :

mk ↑(⋃ (i : ι), f i) ≤ sum fun (i : ι) => mk ↑(f i)

theorem Cardinal.mk_iUnion_le_sum_mk_lift {α : Type u} {ι : Type v} {f : ι → Set α} :

lift.{v, u} (mk ↑(⋃ (i : ι), f i)) ≤ sum fun (i : ι) => mk ↑(f i)

theorem Cardinal.mk_iUnion_eq_sum_mk {α ι : Type u} {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) :

mk ↑(⋃ (i : ι), f i) = sum fun (i : ι) => mk ↑(f i)

theorem Cardinal.mk_iUnion_eq_sum_mk_lift {α : Type u} {ι : Type v} {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) :

lift.{v, u} (mk ↑(⋃ (i : ι), f i)) = sum fun (i : ι) => mk ↑(f i)

theorem Cardinal.mk_iUnion_le {α ι : Type u} (f : ι → Set α) :

mk ↑(⋃ (i : ι), f i) ≤ mk ι * ⨆ (i : ι), mk ↑(f i)

theorem Cardinal.mk_iUnion_le_lift {α : Type u} {ι : Type v} (f : ι → Set α) :

lift.{v, u} (mk ↑(⋃ (i : ι), f i)) ≤ lift.{u, v} (mk ι) * ⨆ (i : ι), lift.{v, u} (mk ↑(f i))

theorem Cardinal.mk_sUnion_le {α : Type u} (A : Set (Set α)) :

mk ↑(⋃₀ A) ≤ mk ↑A * ⨆ (s : ↑A), mk ↑↑s

theorem Cardinal.mk_biUnion_le {ι α : Type u} (A : ι → Set α) (s : Set ι) :

mk ↑(⋃ x ∈ s, A x) ≤ mk ↑s * ⨆ (x : ↑s), mk ↑(A ↑x)

theorem Cardinal.mk_biUnion_le_lift {α : Type u} {ι : Type v} (A : ι → Set α) (s : Set ι) :

lift.{v, u} (mk ↑(⋃ x ∈ s, A x)) ≤ lift.{u, v} (mk ↑s) * ⨆ (x : ↑s), lift.{v, u} (mk ↑(A ↑x))

theorem Cardinal.finset_card_lt_aleph0 {α : Type u} (s : Finset α) :

mk ↑↑s < aleph0

theorem Cardinal.mk_set_eq_nat_iff_finset {α : Type u_1} {s : Set α} {n : ℕ} :

mk ↑s = ↑n ↔ ∃ (t : Finset α), ↑t = s ∧ t.card = n

theorem Cardinal.mk_eq_nat_iff_finset {α : Type u} {n : ℕ} :

mk α = ↑n ↔ ∃ (t : Finset α), ↑t = Set.univ ∧ t.card = n

theorem Cardinal.mk_eq_nat_iff_fintype {α : Type u} {n : ℕ} :

mk α = ↑n ↔ ∃ (h : Fintype α), Fintype.card α = n

theorem Cardinal.mk_set_eq_one_iff {α : Type u} {s : Set α} :

mk ↑s = 1 ↔ ∃ (x : α), s = {x}

theorem Cardinal.mk_union_add_mk_inter {α : Type u} {S T : Set α} :

mk ↑(S ∪ T) + mk ↑(S ∩ T) = mk ↑S + mk ↑T

theorem Cardinal.mk_union_le {α : Type u} (S T : Set α) :

mk ↑(S ∪ T) ≤ mk ↑S + mk ↑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 : Disjoint S T) :

mk ↑(S ∪ T) = mk ↑S + mk ↑T

theorem Cardinal.mk_insert {α : Type u} {s : Set α} {a : α} (h : a ∉ s) :

mk ↑(insert a s) = mk ↑s + 1

theorem Cardinal.mk_insert_le {α : Type u} {s : Set α} {a : α} :

mk ↑(insert a s) ≤ mk ↑s + 1

theorem Cardinal.mk_sum_compl {α : Type u_1} (s : Set α) :

mk ↑s + mk ↑sᶜ = mk α

theorem Cardinal.mk_le_iff_forall_finset_subset_card_le {α : Type u} {n : ℕ} {t : Set α} :

mk ↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n

theorem Cardinal.mk_subtype_mono {α : Type u} {p q : α → Prop} (h : ∀ (x : α), p x → q x) :

mk { x : α // p x } ≤ mk { x : α // q x }

theorem Cardinal.card_lt_card_of_right_finite {α : Type u} {A B : Set α} (hfin : B.Finite) (hlt : A ⊂ B) :

mk ↑A < mk ↑B

theorem Cardinal.card_lt_card_of_left_finite {α : Type u} {A B : Set α} (hfin : A.Finite) (hlt : A ⊂ B) :

mk ↑A < mk ↑B

theorem Cardinal.mk_strictMono {α : Type u} [Finite α] :

StrictMono (mk ∘ Set.Elem)

theorem Cardinal.mk_strictMonoOn {α : Type u} :

StrictMonoOn (mk ∘ Set.Elem) {s : Set α | s.Finite}

theorem Cardinal.le_mk_diff_add_mk {α : Type u} (S T : Set α) :

mk ↑S ≤ mk ↑(S \ T) + mk ↑T

theorem Cardinal.mk_diff_add_mk {α : Type u} {S T : Set α} (h : T ⊆ S) :

mk ↑(S \ T) + mk ↑T = mk ↑S

theorem Cardinal.diff_nonempty_of_mk_lt_mk {α : Type u} {S T : Set α} (h : mk ↑S < mk ↑T) :

(T \ S).Nonempty

theorem Cardinal.compl_nonempty_of_mk_lt_mk {α : Type u} {S : Set α} (h : mk ↑S < mk α) :

theorem Cardinal.mk_union_le_aleph0 {α : Type u_1} {P Q : Set α} :

mk ↑(P ∪ Q) ≤ aleph0 ↔ mk ↑P ≤ aleph0 ∧ mk ↑Q ≤ aleph0

theorem Cardinal.mk_sep {α : Type u} (s : Set α) (t : α → Prop) :

mk ↑{x : α | x ∈ s ∧ t x} = mk ↑{x : ↑s | t ↑x}

theorem Cardinal.mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β) (h : Function.Injective f) :

lift.{v, u} (mk ↑(f ⁻¹' s)) ≤ lift.{u, v} (mk ↑s)

theorem Cardinal.mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β) (h : s ⊆ Set.range f) :

lift.{u, v} (mk ↑s) ≤ lift.{v, u} (mk ↑(f ⁻¹' s))

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) :

lift.{v, u} (mk ↑(f ⁻¹' s)) = lift.{u, v} (mk ↑s)

theorem Cardinal.mk_preimage_of_injective_of_subset_range {α β : Type u} (f : α → β) (s : Set β) (h : Function.Injective f) (h2 : s ⊆ Set.range f) :

mk ↑(f ⁻¹' s) = mk ↑s

@[simp]

theorem Cardinal.mk_preimage_equiv_lift {α : Type u} {β : Type v} (f : α ≃ β) (s : Set β) :

lift.{v, u} (mk ↑(⇑f ⁻¹' s)) = lift.{u, v} (mk ↑s)

@[simp]

theorem Cardinal.mk_preimage_equiv {α β : Type u} (f : α ≃ β) (s : Set β) :

mk ↑(⇑f ⁻¹' s) = mk ↑s

theorem Cardinal.mk_preimage_of_injective {α β : Type u} (f : α → β) (s : Set β) (h : Function.Injective f) :

mk ↑(f ⁻¹' s) ≤ mk ↑s

theorem Cardinal.mk_preimage_of_subset_range {α β : Type u} (f : α → β) (s : Set β) (h : s ⊆ Set.range f) :

mk ↑s ≤ mk ↑(f ⁻¹' s)

theorem Cardinal.mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : Set α} {t : Set β} (h : t ⊆ f '' s) :

lift.{u, v} (mk ↑t) ≤ lift.{v, u} (mk ↑{x : α | x ∈ s ∧ f x ∈ t})

theorem Cardinal.mk_subset_ge_of_subset_image {α β : Type u} (f : α → β) {s : Set α} {t : Set β} (h : t ⊆ f '' s) :

mk ↑t ≤ mk ↑{x : α | x ∈ s ∧ f x ∈ t}

theorem Cardinal.le_mk_iff_exists_subset {c : Cardinal.{u}} {α : Type u} {s : Set α} :

c ≤ mk ↑s ↔ ∃ p ⊆ s, mk ↑p = c

@[simp]

theorem Cardinal.mk_range_inl {α : Type u} {β : Type v} :

mk ↑(Set.range Sum.inl) = lift.{v, u} (mk α)

@[simp]

theorem Cardinal.mk_range_inr {α : Type u} {β : Type v} :

mk ↑(Set.range Sum.inr) = lift.{u, v} (mk β)

theorem Cardinal.two_le_iff {α : Type u} :

2 ≤ mk α ↔ ∃ (x : α) (y : α), x ≠ y

theorem Cardinal.two_le_iff' {α : Type u} (x : α) :

2 ≤ mk α ↔ ∃ (y : α), y ≠ x

theorem Cardinal.mk_eq_two_iff {α : Type u} :

mk α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ {x, y} = Set.univ

theorem Cardinal.mk_eq_two_iff' {α : Type u} (x : α) :

mk α = 2 ↔ ∃! y : α, y ≠ x

theorem Cardinal.exists_notMem_of_length_lt {α : Type u_1} (l : List α) (h : ↑l.length < mk α) :

∃ (z : α), z ∉ l

theorem Cardinal.exists_ne_ne_of_three_le {α : Type u_1} (h : 3 ≤ mk α) (x y : α) :

∃ (z : α), z ≠ x ∧ z ≠ y

@[deprecated Cardinal.exists_ne_ne_of_three_le (since := "2026-02-17")]

theorem Cardinal.three_le {α : Type u_1} (h : 3 ≤ mk α) (x y : α) :

∃ (z : α), z ≠ x ∧ z ≠ y

Alias of Cardinal.exists_ne_ne_of_three_le.

`powerlt` operation #

noncomputable def Cardinal.powerlt (a b : Cardinal.{u}) :

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

Equations

a ^< b = ⨆ (c : ↑(Set.Iio b)), a ^ ↑c

Instances For

def Cardinal.«term_^<_» :

Lean.TrailingParserDescr

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

Equations

Cardinal.«term_^<_» = Lean.ParserDescr.trailingNode `Cardinal.«term_^<_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^< ") (Lean.ParserDescr.cat `term 81))

Instances For

theorem Cardinal.le_powerlt {b c : Cardinal.{u}} (a : Cardinal.{u}) (h : c < b) :

a ^ c ≤ a ^< b

theorem Cardinal.powerlt_le {a b c : Cardinal.{u}} :

a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

theorem Cardinal.powerlt_le_powerlt_left {a b c : Cardinal.{u_1}} (h : b ≤ c) :

a ^< b ≤ a ^< c

theorem Cardinal.powerlt_mono_left (a : Cardinal.{u_1}) :

Monotone fun (c : Cardinal.{u_1}) => a ^< c

theorem Cardinal.powerlt_succ {a b : Cardinal.{u_1}} (h : a ≠ 0) :

a ^< Order.succ b = a ^ b

theorem Cardinal.powerlt_min {a b c : Cardinal.{u_1}} :

a ^< min b c = min (a ^< b) (a ^< c)

theorem Cardinal.powerlt_max {a b c : Cardinal.{u_1}} :

a ^< max b c = max (a ^< b) (a ^< c)

theorem Cardinal.zero_powerlt {a : Cardinal.{u_1}} (h : a ≠ 0) :

0 ^< a = 1

@[simp]

theorem Cardinal.powerlt_zero {a : Cardinal.{u_1}} :

a ^< 0 = 0

theorem WellFounded.cardinalMk_subtype_lt_min_compl_le {α : Type u} {r : α → α → Prop} (wf : WellFounded r) {s : Set α} (hs : sᶜ.Nonempty) :

Cardinal.mk { x : α // r x (wf.min sᶜ hs) } ≤ Cardinal.mk ↑s

The cardinality of a set is an upper-bound for the amount of elements before the set's mex (minimum excluded value)