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