neg_eq_top — Mathlib

English

In a linear ordered additive group with top, the negation of an element equals the top element only when the element itself is top: -a = ⊤ iff a = ⊤.

Русский

В линейно упорядоченной абелевой группе с верхней границей отрицание элемента равно верхнему элементу тогда и только тогда, когда сам элемент равен верхнему.

LaTeX

$$$-a = \top \iff a = \top$$$

Lean4

@[simp]
theorem neg_eq_top {a : α} : -a = ⊤ ↔ a = ⊤
    where
  mp
    h := by
    by_contra nh
    replace nh := add_neg_cancel_of_ne_top nh
    rw [h, add_top] at nh
    exact top_ne_zero nh
  mpr h := by simp [h]

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