add_ne_top_iff_ne_top_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem add_ne_top_iff_ne_top_left {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : x + y ≠ ⊤ ↔ x ≠ ⊤ := by
  cases x <;> simp [add_ne_top_iff_ne_top₂, hy, hy']

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