Order on cardinal numbers

We define the order on cardinal numbers and show its basic properties, including the ordered semiring structure.

Main definitions

• The order c₁ ≤ c₂ is defined by Cardinal.le_def α β : #α ≤ #β ↔ Nonempty (α ↪ β).
• Order.IsSuccLimit c means that c is a (weak) limit cardinal: c ≠ 0 ∧ ∀ x < c, succ x < c.
• Cardinal.IsStrongLimit c means that c is a strong limit cardinal: c ≠ 0 ∧ ∀ x < c, 2 ^ x < c.

Main instances

• Cardinals form a CanonicallyOrderedAdd OrderedCommSemiring with the aforementioned sum and product.
• Cardinals form a SuccOrder. Use Order.succ c for the smallest cardinal greater than c.
• The less than relation on cardinals forms a well-order.
• Cardinals form a ConditionallyCompleteLinearOrderBot. Bounded sets for cardinals in universe u are precisely the sets indexed by some type in universe u, see Cardinal.bddAbove_iff_small (in Mathlib.SetTheory.Cardinal.Small). One can use sSup for the cardinal supremum, and sInf 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

The current setup interweaves the order structure and the algebraic structure on Cardinal tightly. For example, we need to know what a ring is in order to show that 0 is the smallest cardinality. That is reflected in this file containing both the order and algebra structure.

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

Order on cardinals

instance Cardinal.instLE : LE Cardinal.{u}

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

Equations

• Cardinal.instLE = { le := fun (q₁ q₂ : Cardinal.{?u.28}) => Quotient.liftOn₂ q₁ q₂ (fun (α β : Type ?u.28) => Nonempty (α ↪ β)) Cardinal.instLE.proof_1 }

instance Cardinal.partialOrder : PartialOrder Cardinal.{u}

Equations

• Cardinal.partialOrder = PartialOrder.mk Cardinal.partialOrder.proof_4

instance Cardinal.linearOrder : LinearOrder Cardinal.{u}

Equations

• One or more equations did not get rendered due to their size.

theorem Cardinal.le_def (α β : Type u) : mk α ≤ mk β ↔ Nonempty (α ↪ β)

theorem Cardinal.mk_le_of_injective {α β : Type u} {f : α → β} (hf : Function.Injective f) : mk α ≤ mk β

theorem Function.Embedding.cardinal_le {α β : Type u} (f : α ↪ β) : Cardinal.mk α ≤ Cardinal.mk β

theorem Cardinal.mk_le_of_surjective {α β : Type u} {f : α → β} (hf : Function.Surjective f) : mk β ≤ mk α

theorem Cardinal.le_mk_iff_exists_set {c : Cardinal.{u}} {α : Type u} : c ≤ mk α ↔ ∃ (p : Set α), mk ↑p = c

theorem Cardinal.mk_subtype_le {α : Type u} (p : α → Prop) : mk (Subtype p) ≤ mk α

theorem Cardinal.mk_set_le {α : Type u} (s : Set α) : mk ↑s ≤ mk α

theorem Cardinal.out_embedding {c c' : Cardinal.{u_1}} : c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')

theorem Cardinal.lift_mk_le {α : Type v} {β : Type w} : lift.{max u w, v} (mk α) ≤ lift.{max u v, w} (mk β) ↔ Nonempty (α ↪ β)

theorem Cardinal.lift_mk_le' {α : Type u} {β : Type v} : lift.{v, u} (mk α) ≤ lift.{u, v} (mk β) ↔ 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.

lift sends Cardinal.{u} to an initial segment of Cardinal.{max u v}.

def Cardinal.liftInitialSeg : InitialSeg (fun (x1 x2 : Cardinal.{u}) => x1 < x2) fun (x1 x2 : Cardinal.{max u v}) => x1 < x2

Cardinal.lift as an InitialSeg.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cardinal.liftInitialSeg_toFun (c : Cardinal.{u}) : liftInitialSeg c = lift.{v, u} c

theorem Cardinal.mem_range_lift_of_le {a : Cardinal.{u}} {b : Cardinal.{max u v}} : b ≤ lift.{v, u} a → b ∈ Set.range lift.{v, u}

@[deprecated Cardinal.mem_range_lift_of_le (since := "2024-10-07")]

theorem Cardinal.lift_down {a : Cardinal.{u}} {b : Cardinal.{max u v}} : b ≤ lift.{v, u} a → ∃ (a' : Cardinal.{u}), lift.{v, u} a' = b

@[deprecated Cardinal.liftInitialSeg (since := "2024-10-07")]

def Cardinal.liftOrderEmbedding : Cardinal.{v} ↪o Cardinal.{max v u}

Cardinal.lift as an OrderEmbedding.

Equations

• Cardinal.liftOrderEmbedding = Cardinal.liftInitialSeg.toOrderEmbedding

theorem Cardinal.lift_injective : Function.Injective lift.{u, v}

@[simp]

theorem Cardinal.lift_inj {a b : Cardinal.{u}} : lift.{v, u} a = lift.{v, u} b ↔ a = b

@[simp]

theorem Cardinal.lift_le {a b : Cardinal.{v}} : lift.{u, v} a ≤ lift.{u, v} b ↔ a ≤ b

@[simp]

theorem Cardinal.lift_lt {a b : Cardinal.{u}} : lift.{v, u} a < lift.{v, u} b ↔ a < b

theorem Cardinal.lift_strictMono : StrictMono lift.{u_2, u_1}

theorem Cardinal.lift_monotone : Monotone lift.{u_2, u_1}

@[simp]

theorem Cardinal.lift_min {a b : Cardinal.{v}} : lift.{u, v} (a ⊓ b) = lift.{u, v} a ⊓ lift.{u, v} b

@[simp]

theorem Cardinal.lift_max {a b : Cardinal.{v}} : lift.{u, v} (a ⊔ b) = lift.{u, v} a ⊔ lift.{u, v} b

@[simp]

theorem Cardinal.lift_umax_eq {a : Cardinal.{u}} {b : Cardinal.{v}} : lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b

theorem Cardinal.le_lift_iff {a : Cardinal.{u}} {b : Cardinal.{max u v}} : b ≤ lift.{v, u} a ↔ ∃ a' ≤ a, lift.{v, u} a' = b

theorem Cardinal.lt_lift_iff {a : Cardinal.{u}} {b : Cardinal.{max u v}} : b < lift.{v, u} a ↔ ∃ a' < a, lift.{v, u} a' = b

Basic cardinals

@[simp]

theorem Cardinal.lift_eq_zero {a : Cardinal.{v}} : lift.{u, v} a = 0 ↔ a = 0

@[simp]

theorem Cardinal.mk_fintype (α : Type u) [h : Fintype α] : mk α = ↑(Fintype.card α)

instance Cardinal.commSemiring : CommSemiring Cardinal.{u}

Equations

• Cardinal.commSemiring = CommSemiring.mk Cardinal.commSemiring.proof_16

theorem Cardinal.mk_bool : mk Bool = 2

theorem Cardinal.mk_Prop : mk Prop = 2

theorem Cardinal.power_mul {a b c : Cardinal.{u_1}} : a ^ (b * c) = (a ^ b) ^ c

@[simp]

theorem Cardinal.power_natCast (a : Cardinal.{u}) (n : ℕ) : a ^ ↑n = a ^ n

@[deprecated Cardinal.power_natCast (since := "2024-10-16")]

theorem Cardinal.power_cast_right (a : Cardinal.{u}) (n : ℕ) : a ^ ↑n = a ^ n

Alias of Cardinal.power_natCast.

@[simp]

theorem Cardinal.lift_eq_one {a : Cardinal.{v}} : lift.{u, v} a = 1 ↔ a = 1

@[simp]

theorem Cardinal.lift_mul (a b : Cardinal.{u}) : lift.{v, u} (a * b) = lift.{v, u} a * lift.{v, u} b

theorem Cardinal.lift_two : lift.{u, v} 2 = 2

@[simp]

theorem Cardinal.mk_set {α : Type u} : mk (Set α) = 2 ^ mk α

@[simp]

theorem Cardinal.mk_powerset {α : Type u} (s : Set α) : mk ↑(𝒫 s) = 2 ^ mk ↑s

A variant of Cardinal.mk_set expressed in terms of a Set instead of a Type.

theorem Cardinal.lift_two_power (a : Cardinal.{u_1}) : lift.{v, u_1} (2 ^ a) = 2 ^ lift.{v, u_1} a

Order properties

theorem Cardinal.zero_le (a : Cardinal.{u_1}) : 0 ≤ a

instance Cardinal.addLeftMono : AddLeftMono Cardinal.{u_1}

instance Cardinal.addRightMono : AddRightMono Cardinal.{u_1}

instance Cardinal.canonicallyOrderedAdd : CanonicallyOrderedAdd Cardinal.{u}

instance Cardinal.orderedCommSemiring : OrderedCommSemiring Cardinal.{u}

Equations

• Cardinal.orderedCommSemiring = CanonicallyOrderedAdd.toOrderedCommSemiring

instance Cardinal.instLinearOrderedAddCommMonoid : LinearOrderedAddCommMonoid Cardinal.{u}

Equations

• Cardinal.instLinearOrderedAddCommMonoid = LinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Cardinal.orderBot : OrderBot Cardinal.{u}

Equations

• Cardinal.orderBot = inferInstance

instance Cardinal.noZeroDivisors : NoZeroDivisors Cardinal.{u}

instance Cardinal.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero Cardinal.{u}

Equations

• One or more equations did not get rendered due to their size.

instance Cardinal.instCommMonoidWithZero : CommMonoidWithZero Cardinal.{u}

Equations

• Cardinal.instCommMonoidWithZero = CommMonoidWithZero.mk Cardinal.instCommMonoidWithZero.proof_6 Cardinal.instCommMonoidWithZero.proof_7

instance Cardinal.instCommMonoid : CommMonoid Cardinal.{u}

Equations

• Cardinal.instCommMonoid = CommMonoid.mk ⋯

theorem Cardinal.zero_power_le (c : Cardinal.{u}) : 0 ^ c ≤ 1

theorem Cardinal.power_le_power_left {a b c : Cardinal.{u_1}} : a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

theorem Cardinal.self_le_power (a : Cardinal.{u_1}) {b : Cardinal.{u_1}} (hb : 1 ≤ b) : a ≤ a ^ b

theorem Cardinal.cantor (a : Cardinal.{u}) : a < 2 ^ a

Cantor's theorem

instance Cardinal.instNoMaxOrder : NoMaxOrder Cardinal.{u}

instance Cardinal.instDistribLattice : DistribLattice Cardinal.{u}

Equations

• Cardinal.instDistribLattice = inferInstance

theorem Cardinal.power_le_max_power_one {a b c : Cardinal.{u_1}} (h : b ≤ c) : a ^ b ≤ a ^ c ⊔ 1

theorem Cardinal.power_le_power_right {a b c : Cardinal.{u_1}} : a ≤ b → a ^ c ≤ b ^ c

theorem Cardinal.power_pos {a : Cardinal.{u_1}} (b : Cardinal.{u_1}) (ha : 0 < a) : 0 < a ^ b

theorem Cardinal.lt_wf : WellFounded fun (x1 x2 : Cardinal.{u}) => x1 < x2

instance Cardinal.instWellFoundedRelation : WellFoundedRelation Cardinal.{u}

Equations

• Cardinal.instWellFoundedRelation = { rel := fun (x1 x2 : Cardinal.{?u.5}) => x1 < x2, wf := Cardinal.lt_wf }

instance Cardinal.instWellFoundedLT : WellFoundedLT Cardinal.{u}

instance Cardinal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot Cardinal.{u_1}

Equations

• Cardinal.instConditionallyCompleteLinearOrderBot = WellFoundedLT.conditionallyCompleteLinearOrderBot Cardinal.{?u.3}

@[simp]

theorem Cardinal.sInf_empty : sInf ∅ = 0

instance Cardinal.instSuccOrder : SuccOrder Cardinal.{u_1}

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

Equations

• Cardinal.instSuccOrder = ConditionallyCompleteLinearOrder.toSuccOrder

theorem Cardinal.succ_def (c : Cardinal.{u_1}) : Order.succ c = sInf {c' : Cardinal.{u_1} | c < c'}

theorem Cardinal.succ_pos (c : Cardinal.{u_1}) : 0 < Order.succ c

theorem Cardinal.succ_ne_zero (c : Cardinal.{u_1}) : Order.succ c ≠ 0

theorem Cardinal.add_one_le_succ (c : Cardinal.{u}) : c + 1 ≤ Order.succ c

@[simp]

theorem Cardinal.lift_succ (a : Cardinal.{u}) : lift.{v, u} (Order.succ a) = Order.succ (lift.{v, u} a)

Limit cardinals

@[deprecated Order.IsSuccLimit (since := "2024-09-17")]

def Cardinal.IsLimit (c : Cardinal.{u_1}) : 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. Deprecated. Use Order.IsSuccLimit instead.

Equations

• c.IsLimit = (c ≠ 0 ∧ Order.IsSuccPrelimit c)

theorem Cardinal.ne_zero_of_isSuccLimit {c : ℕ} (h : Order.IsSuccLimit c) : c ≠ 0

theorem Cardinal.isSuccPrelimit_zero : Order.IsSuccPrelimit 0

theorem Cardinal.isSuccLimit_iff {c : Cardinal.{u_1}} : Order.IsSuccLimit c ↔ c ≠ 0 ∧ Order.IsSuccPrelimit c

@[deprecated Order.IsSuccLimit.isSuccPrelimit (since := "2024-09-17")]

theorem Cardinal.IsLimit.isSuccPrelimit {c : Cardinal.{u_1}} (h : c.IsLimit) : Order.IsSuccPrelimit c

@[deprecated Cardinal.ne_zero_of_isSuccLimit (since := "2024-09-17")]

theorem Cardinal.IsLimit.ne_zero {c : Cardinal.{u_1}} (h : c.IsLimit) : c ≠ 0

@[deprecated Cardinal.IsLimit.isSuccPrelimit (since := "2024-09-05")]

theorem Cardinal.IsLimit.isSuccLimit {c : Cardinal.{u_1}} (h : c.IsLimit) : Order.IsSuccPrelimit c

Alias of Cardinal.IsLimit.isSuccPrelimit.

@[deprecated Order.IsSuccLimit.succ_lt (since := "2024-09-17")]

theorem Cardinal.IsLimit.succ_lt {x c : Cardinal.{u_1}} (h : c.IsLimit) : x < c → Order.succ x < c

@[deprecated Cardinal.isSuccPrelimit_zero (since := "2024-09-05")]

theorem Cardinal.isSuccLimit_zero : Order.IsSuccPrelimit 0

Alias of Cardinal.isSuccPrelimit_zero.

structure Cardinal.IsStrongLimit (c : Cardinal.{u_1}) : Prop

A cardinal is a strong limit if it is not zero and it is closed under powersets. Note that ℵ₀ is a strong limit by this definition.

• ne_zero : c ≠ 0
• two_power_lt ⦃x : Cardinal.{u_1}⦄ : x < c → 2 ^ x < c

theorem Cardinal.IsStrongLimit.isSuccLimit {c : Cardinal.{u_1}} (H : c.IsStrongLimit) : Order.IsSuccLimit c

theorem Cardinal.IsStrongLimit.isSuccPrelimit {c : Cardinal.{u_1}} (H : c.IsStrongLimit) : Order.IsSuccPrelimit c

@[deprecated Cardinal.IsStrongLimit.isSuccLimit (since := "2024-09-17")]

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

Indexed cardinal sum

theorem Cardinal.le_sum {ι : Type u_1} (f : ι → Cardinal.{max u_1 u_2}) (i : ι) : f i ≤ sum f

theorem Cardinal.iSup_le_sum {ι : Type u_1} (f : ι → Cardinal.{max u_1 u_2}) : iSup f ≤ sum f

@[simp]

theorem Cardinal.sum_add_distrib {ι : Type u_1} (f g : ι → Cardinal.{u_2}) : sum (f + g) = sum f + sum g

@[simp]

theorem Cardinal.sum_add_distrib' {ι : Type u_1} (f g : ι → Cardinal.{u_2}) : (sum fun (i : ι) => f i + g i) = sum f + sum g

theorem Cardinal.sum_le_sum {ι : Type u_1} (f g : ι → Cardinal.{u_2}) (H : ∀ (i : ι), f i ≤ g i) : sum f ≤ sum g

theorem Cardinal.mk_le_mk_mul_of_mk_preimage_le {α β : Type u} {c : Cardinal.{u}} (f : α → β) (hf : ∀ (b : β), mk ↑(f ⁻¹' {b}) ≤ c) : mk α ≤ mk β * c

theorem Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le {α : Type u} {β : Type v} {c : Cardinal.{max u v}} (f : α → β) (hf : ∀ (b : β), lift.{v, u} (mk ↑(f ⁻¹' {b})) ≤ c) : lift.{v, u} (mk α) ≤ lift.{u, v} (mk β) * c

Well-ordering theorem

theorem nonempty_embedding_to_cardinal {α : Type u} : Nonempty (α ↪ Cardinal.{u})

def embeddingToCardinal {α : Type u} : α ↪ Cardinal.{u}

An embedding of any type to the set of cardinals in its universe.

Equations

• embeddingToCardinal = Classical.choice ⋯

def WellOrderingRel {α : Type u} : α → α → Prop

Any type can be endowed with a well order, obtained by pulling back the well order over cardinals by some embedding.

Equations

• WellOrderingRel = ⇑embeddingToCardinal ⁻¹'o fun (x1 x2 : Cardinal.{?u.23}) => x1 < x2

instance WellOrderingRel.isWellOrder {α : Type u} : IsWellOrder α WellOrderingRel

instance IsWellOrder.subtype_nonempty {α : Type u} : Nonempty { r : α → α → Prop // IsWellOrder α r }

theorem exists_wellOrder (α : Type u) : ∃ (x : LinearOrder α), WellFoundedLT α

The well-ordering theorem (or Zermelo's theorem): every type has a well-order

Bounds on suprema

theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccPrelimit {ι : Type u} (f : ι → Cardinal.{v}) (ω : Cardinal.{v}) (hω : ¬Order.IsSuccPrelimit ω) (h : ⨆ (i : ι), f i = ω) : ∃ (i : ι), f i = ω

theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (Set.range f)) {c : Cardinal.{v}} (hc : ¬Order.IsSuccLimit c) (h : ⨆ (i : ι), f i = c) : ∃ (i : ι), f i = c

@[deprecated Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit (since := "2024-09-17")]

theorem Cardinal.exists_eq_of_iSup_eq_of_not_isLimit {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (Set.range f)) (ω : Cardinal.{v}) (hω : ¬ω.IsLimit) (h : ⨆ (i : ι), f i = ω) : ∃ (i : ι), f i = ω

Indexed cardinal prod

theorem Cardinal.sum_lt_prod {ι : Type u_1} (f g : ι → Cardinal.{u_2}) (H : ∀ (i : ι), f i < g i) : sum f < prod g

König's theorem

theorem Cardinal.prod_le_prod {ι : Type u_1} (f g : ι → Cardinal.{u_2}) (H : ∀ (i : ι), f i ≤ g i) : prod f ≤ prod g

The first infinite cardinal aleph0

theorem Cardinal.aleph0_pos : 0 < aleph0

@[simp]

theorem Cardinal.aleph0_le_lift {c : Cardinal.{u}} : aleph0 ≤ lift.{v, u} c ↔ aleph0 ≤ c

@[simp]

theorem Cardinal.lift_le_aleph0 {c : Cardinal.{u}} : lift.{v, u} c ≤ aleph0 ↔ c ≤ aleph0

@[simp]

theorem Cardinal.aleph0_lt_lift {c : Cardinal.{u}} : aleph0 < lift.{v, u} c ↔ aleph0 < c

@[simp]

theorem Cardinal.lift_lt_aleph0 {c : Cardinal.{u}} : lift.{v, u} c < aleph0 ↔ c < aleph0

@[simp]

theorem Cardinal.aleph0_eq_lift {c : Cardinal.{u}} : aleph0 = lift.{v, u} c ↔ aleph0 = c

@[simp]

theorem Cardinal.lift_eq_aleph0 {c : Cardinal.{u}} : lift.{v, u} c = aleph0 ↔ c = aleph0

Properties about the cast from ℕ

theorem Cardinal.mk_fin (n : ℕ) : mk (Fin n) = ↑n

@[simp]

theorem Cardinal.lift_natCast (n : ℕ) : lift.{u, v} ↑n = ↑n

@[simp]

theorem Cardinal.lift_ofNat (n : ℕ) [n.AtLeastTwo] : lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Cardinal.lift_eq_nat_iff {a : Cardinal.{u}} {n : ℕ} : lift.{v, u} a = ↑n ↔ a = ↑n

@[simp]

theorem Cardinal.lift_eq_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v, u} a = OfNat.ofNat n ↔ a = OfNat.ofNat n

@[simp]

theorem Cardinal.nat_eq_lift_iff {n : ℕ} {a : Cardinal.{u}} : ↑n = lift.{v, u} a ↔ ↑n = a

@[simp]

theorem Cardinal.zero_eq_lift_iff {a : Cardinal.{u}} : 0 = lift.{v, u} a ↔ 0 = a

@[simp]

theorem Cardinal.one_eq_lift_iff {a : Cardinal.{u}} : 1 = lift.{v, u} a ↔ 1 = a

@[simp]

theorem Cardinal.ofNat_eq_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n = lift.{v, u} a ↔ OfNat.ofNat n = a

@[simp]

theorem Cardinal.lift_le_nat_iff {a : Cardinal.{u}} {n : ℕ} : lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n

@[simp]

theorem Cardinal.lift_le_one_iff {a : Cardinal.{u}} : lift.{v, u} a ≤ 1 ↔ a ≤ 1

@[simp]

theorem Cardinal.lift_le_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v, u} a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n

@[simp]

theorem Cardinal.nat_le_lift_iff {n : ℕ} {a : Cardinal.{u}} : ↑n ≤ lift.{v, u} a ↔ ↑n ≤ a

@[simp]

theorem Cardinal.one_le_lift_iff {a : Cardinal.{u}} : 1 ≤ lift.{v, u} a ↔ 1 ≤ a

@[simp]

theorem Cardinal.ofNat_le_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n ≤ lift.{v, u} a ↔ OfNat.ofNat n ≤ a

@[simp]

theorem Cardinal.lift_lt_nat_iff {a : Cardinal.{u}} {n : ℕ} : lift.{v, u} a < ↑n ↔ a < ↑n

@[simp]

theorem Cardinal.lift_lt_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v, u} a < OfNat.ofNat n ↔ a < OfNat.ofNat n

@[simp]

theorem Cardinal.nat_lt_lift_iff {n : ℕ} {a : Cardinal.{u}} : ↑n < lift.{v, u} a ↔ ↑n < a

@[simp]

theorem Cardinal.zero_lt_lift_iff {a : Cardinal.{u}} : 0 < lift.{v, u} a ↔ 0 < a

@[simp]

theorem Cardinal.one_lt_lift_iff {a : Cardinal.{u}} : 1 < lift.{v, u} a ↔ 1 < a

@[simp]

theorem Cardinal.ofNat_lt_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n < lift.{v, u} a ↔ OfNat.ofNat n < a

theorem Cardinal.mk_coe_finset {α : Type u} {s : Finset α} : mk { x : α // x ∈ s } = ↑s.card

theorem Cardinal.card_le_of_finset {α : Type u_1} (s : Finset α) : ↑s.card ≤ mk α

instance Cardinal.instCharZero : CharZero Cardinal.{u_1}