ofNat_lt_ofENat — Mathlib

English

For natural m with at least two, and for n in ENat, the inequality between their embeddings into Cardinal corresponds to inequality in ENat: (ofNat m) < n in Cardinal iff OfNat.ofNat m < n.

Русский

Для натурального m, имеющего хотя бы два, и для n в ENat, неравенство их отображения в Cardinal равно неравенству в ENat.

LaTeX

$$$ (\mathrm{ofNat}(m) : \mathrm{Cardinal}) < n \iff \mathrm{OfNat.ofNat}(m) < n $$$

Lean4

@[simp, norm_cast]
theorem ofNat_lt_ofENat {m : ℕ} [m.AtLeastTwo] {n : ℕ∞} : (ofNat(m) : Cardinal) < n ↔ OfNat.ofNat m < n :=
  nat_lt_ofENat

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