not_ofNat_lt_one

Mathlib.Data.Nat.Cast.Order.Basic

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

English

If n ≥ 2, then (ofNat(n) : α) < 1 is false.

Русский

Если n ≥ 2, то (ofNat(n) : α) < 1 ложно.

LaTeX

$$$\forall n \in \mathbb{N},\ n \ge 2 \Rightarrow \neg\big((\mathrm{ofNat}(n) : \alpha) < 1\big).$$$

Lean4

@[simp]
theorem not_ofNat_lt_one : ¬(ofNat(n) : α) < 1 :=
  mt le_of_lt not_ofNat_le_one

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

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

Разделы

Аффилиация

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