ofENat_lt_ofNat

Mathlib.SetTheory.Cardinal.ENat

URI: https://scilib.ai/kg/mathlib#Cardinal.ofENat_lt_ofNat

English

For m ∈ ENat and n ∈ Nat with n ≥ 2, (ofENat m) < (ofNat n) iff (OfNat.ofNat n) < m.

Русский

Для m ∈ ENat и n ∈ Nat с n ≥ 2, (ofENat m) < (ofNat n) ⇔ (OfNat.ofNat n) < m.

LaTeX

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

Lean4

@[simp]
theorem ofENat_lt_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] : ofENat m < ofNat(n) ↔ m < OfNat.ofNat n :=
  ofENat_lt_nat

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru