untop₀_nonneg — Mathlib

English

For AddCommGroup α and PartialOrder α, 0 ≤ a.untop₀ iff 0 ≤ a.

Русский

Для AddCommGroup α и PartialOrder α: 0 ≤ a.untop₀ эквивалентно 0 ≤ a.

LaTeX

$$$[AddCommGroup \alpha] [PartialOrder \alpha] \; 0 \le a.untop_0 \iff 0 \le a$$$

Lean4

/-- Elements of ordered additive commutative groups are nonnegative iff their untop₀ is nonnegative.
-/
@[simp]
theorem untop₀_nonneg [AddCommGroup α] [PartialOrder α] {a : WithTop α} : 0 ≤ a.untop₀ ↔ 0 ≤ a := by
  cases a with
  | top => tauto
  | coe a => simp

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