one_le_iff_zero_lt

Mathlib.Data.Nat.WithBot

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

← MathLib Explorer

English

In WithBot ℕ, 1 ≤ x iff 0 < x.

Русский

В WithBot ℕ, 1 ≤ x эквивалентно 0 < x.

LaTeX

$$$1 \le x \iff 0 < x$$$

Lean4

theorem one_le_iff_zero_lt {x : WithBot ℕ} : 1 ≤ x ↔ 0 < x :=
  by
  refine ⟨zero_lt_one.trans_le, fun h => ?_⟩
  cases x
  · exact (not_lt_bot h).elim
  ·
    rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add, ← WithBot.coe_le_coe,
      WithBot.coe_one] at h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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