ofNat_lt_lift_iff — Mathlib

English

For a natural number n with at least two, the cardinal of n via OfNat is less than lift(a) iff the cardinal of n via OfNat is less than a.

Русский

Для натурального n с условием AtLeastTwo: (ofNat n) < lift(a) ⇔ (OfNat.ofNat n) < a.

LaTeX

$$$\left(\mathrm{ofNat}(n) : \mathrm{Cardinal}\right) < \operatorname{lift}(a) \iff \left(\mathrm{OfNat.ofNat} n : \mathrm{Cardinal} \right) < a$$$

Lean4

@[simp]
theorem ofNat_lt_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    (ofNat(n) : Cardinal) < lift.{v} a ↔ (OfNat.ofNat n : Cardinal) < a :=
  nat_lt_lift_iff

Похожие утверждения