nat_lt_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

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

Русский

Для m ∈ Nat и n ∈ ENat, m.cast < Cardinal.ofENat n ⇔ m < n.

LaTeX

$$(m.cast) < (Cardinal.ofENat(n)) \iff m < n$$

Lean4

@[simp]
theorem nat_lt_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) < n ↔ m < n := by norm_cast

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

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

Разделы

Аффилиация

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