add_ne_top_iff_of_ne_bot_of_ne_top

English

If y ≠ ⊥ and y ≠ ⊤, then x+y ≠ ⊤ iff x ≠ ⊤.

Русский

Если y ≠ ⊥ и 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_of_ne_bot_of_ne_top {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : x + y ≠ ⊤ ↔ x ≠ ⊤ := by
  induction x <;> simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

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