ofENat_lt_nat

Mathlib.SetTheory.Cardinal.ENat

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

English

For m ∈ ENat and n ∈ Nat, (m : Cardinal) < n.cast iff m < n.

Русский

Для m ∈ ENat и n ∈ Nat, (m : Cardinal) < n.cast ⇔ m < n.

LaTeX

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

Lean4

@[simp]
theorem ofENat_lt_nat {m : ℕ∞} {n : ℕ} : ofENat m < n ↔ m < n := by norm_cast

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

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

Разделы

Аффилиация

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