one_lt_ofNat

Mathlib.Data.Nat.Cast.Order.Basic

URI: https://scilib.ai/kg/mathlib#Nat.one_lt_ofNat

English

For all n, 1 < (ofNat(n) : α) holds when n ≥ 2.

Русский

Для каждого n: 1 < (ofNat(n) : α) верно, если n ≥ 2.

LaTeX

$$$\forall n \in \mathbb{N},\ 1 < (\mathrm{ofNat}(n) : \alpha).$$$

Lean4

@[simp]
theorem one_lt_ofNat : 1 < (ofNat(n) : α) :=
  one_lt_cast.mpr AtLeastTwo.one_lt

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

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

Разделы

Аффилиация

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