top_add_iff_ne_bot — Mathlib

English

⊤ + x = ⊤ if and only if x ≠ ⊥.

Русский

⊤ + x = ⊤ тогда и только тогда, когда x ≠ ⊥.

LaTeX

$$$\\\\top + x = \\\\top \\\\Leftrightarrow x \\\\neq \\\\bot$$$

Lean4

/-- For any extended real number `x`, the sum of `⊤` and `x` is equal to `⊤`
if and only if `x` is not `⊥`. -/
theorem top_add_iff_ne_bot {x : EReal} : ⊤ + x = ⊤ ↔ x ≠ ⊥ :=
  by
  constructor <;> intro h
  · rintro rfl
    rw [add_bot] at h
    exact bot_ne_top h
  ·
    cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h

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