not_lt_one

Mathlib.Data.PNat.Defs

URI: https://scilib.ai/kg/mathlib#PNat.not_lt_one

English

Let n be a positive natural number. Then n ≥ 1.

Русский

Пусть n — положительное натуральное число. Тогда n ≥ 1.

LaTeX

$$$\\forall n \\in \\mathbb{N}^+,\\ 1 \\le n$$$

Lean4

@[simp]
theorem not_lt_one (n : ℕ+) : ¬n < 1 :=
  not_lt_of_ge n.one_le

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

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

Разделы

Аффилиация

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