one_le_iff_pos — Mathlib

English

For α with a PartialOrder, AddMonoidWithOne, ZeroLEOneClass and SuccAddOrder, for a in WithBot α, 1 ≤ a if and only if 0 < a.

Русский

Для α с частичным порядком, AddMonoidWithOne, ZeroLEOneClass и SuccAddOrder, для a ∈ WithBot α верно: 1 ≤ a тогда и только если 0 < a.

LaTeX

$$$$1 \le a \iff 0 < a,$$$$

Lean4

theorem one_le_iff_pos {α : Type*} [PartialOrder α] [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 : α)]
    [SuccAddOrder α] (a : WithBot α) : 1 ≤ a ↔ 0 < a := by cases a <;> simp [Order.one_le_iff_pos]

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