le_one_iff

Mathlib.Data.PNat.Basic

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

English

Let n be a positive natural number. Then n ≤ 1 if and only if n = 1.

Русский

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

LaTeX

$$$$ \forall n \in \mathbb{N}_{>0},\; n \le 1 \iff n = 1 $$$$

Lean4

@[simp]
theorem le_one_iff {n : ℕ+} : n ≤ 1 ↔ n = 1 :=
  le_bot_iff

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

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

Разделы

Аффилиация

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