add_eq_top — Mathlib

English

Let α be a linear ordered additive commutative group with a top element ⊤. For all a,b ∈ α, we have a + b = ⊤ if and only if a = ⊤ or b = ⊤.

Русский

Пусть α — линейно упорядоченная абелева группа с добавлением и верхней границей ⊤. Для любых a, b ∈ α выполняется a + b = ⊤ тогда и только тогда, когда a = ⊤ или b = ⊤.

LaTeX

$$$a + b = \top \Leftrightarrow a = \top \lor b = \top$$$

Lean4

@[simp]
theorem add_eq_top : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ := by
  constructor
  · intro h
    by_contra nh
    rw [not_or] at nh
    replace h := congrArg (-a + ·) h
    dsimp only at h
    rw [add_top, ← add_assoc, add_comm (-a), add_neg_cancel_of_ne_top, zero_add] at h
    · exact nh.2 h
    · exact nh.1
  · rintro (rfl | rfl)
    · simp
    · simp

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