ofENat_lt_ofENat — Mathlib

English

The strict order on ENat is preserved under the canonical embedding into Cardinal: (m:Cardinal) < n iff m < n for ENat elements.

Русский

Строгое сравнение ENat сохраняется после отображения в Cardinal: (m:Cardinal) < n эквивалентно m < n.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem ofENat_lt_ofENat {m n : ℕ∞} : (m : Cardinal) < n ↔ m < n :=
  ofENat_strictMono.lt_iff_lt

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