nat_eq_lift_iff — Mathlib

English

For a, n with n ≥ 2, lift(a) = OfNat.ofNat(n) iff a = OfNat.ofNat(n).

Русский

Для a и n, при n ≥ 2, lift(a) = OfNat.ofNat(n) эквивалентно a = OfNat.ofNat(n).

LaTeX

$$$\forall a\,\forall n\, [n.AtLeastTwo],\ \operatorname{lift}(a) = \mathrm{instOfNatAtLeastTwo.ofNat}(n) \iff a = \mathrm{instOfNatAtLeastTwo.ofNat}(n)$$$

Lean4

@[simp]
theorem nat_eq_lift_iff {n : ℕ} {a : Cardinal.{u}} : (n : Cardinal) = lift.{v} a ↔ (n : Cardinal) = a := by
  rw [← lift_natCast.{v, u} n, lift_inj]

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