lt_one_iff_le_zero

Mathlib.Data.Nat.WithBot

URI: https://scilib.ai/kg/mathlib#Nat.WithBot.lt_one_iff_le_zero

English

If n < m in WithBot ℕ, then n + 1 ≤ m.

Русский

Если n < m в WithBot ℕ, то n+1 ≤ m.

LaTeX

$$$\forall n,m \in \mathrm{WithBot}\,\mathbb{N},\ n < m \rightarrow n+1 \le m$$$

Lean4

theorem lt_one_iff_le_zero {x : WithBot ℕ} : x < 1 ↔ x ≤ 0 :=
  not_iff_not.mp (by simpa using one_le_iff_zero_lt)

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

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

Разделы

Аффилиация

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