add_ne_top_iff_ne_top_right — Mathlib

English

If x is neither bottom nor top, then x+y ≠ ⊤ if and only if y ≠ ⊤.

Русский

Если x не равен ни ⊥, ни ⊤, то x+y ≠ ⊤ тогда и только тогда, когда y ≠ ⊤.

LaTeX

$$$$\forall x,y\in \mathrm{EReal},\ x \neq \bot \land x \neq \top \Rightarrow (x+y \neq \top \iff y \neq \top).$$$$

Lean4

theorem add_ne_top_iff_ne_top_right {x y : EReal} (hx : x ≠ ⊥) (hx' : x ≠ ⊤) : x + y ≠ ⊤ ↔ y ≠ ⊤ :=
  add_comm x y ▸ add_ne_top_iff_ne_top_left hx hx'

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