coe_lt_coe

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.coe_lt_coe

English

Let n,m be natural numbers. Then (n : ENat) < (m : ENat) iff n < m.

Русский

Пусть n,m ∈ ℕ. Тогда (n: ENat) < (m: ENat) эквивалентно n < m.

LaTeX

$$$\forall {n,m : \mathbb{N}},\ (n : \mathbb{N}_{\infty}) < (m : \mathbb{N}_{\infty}) \;\leftrightarrow\; n < m$$$

Lean4

theorem coe_lt_coe {n m : ℕ} : (n : ℕ∞) < (m : ℕ∞) ↔ n < m := by simp

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

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

Разделы

Аффилиация

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