add_ne_top — Mathlib

English

Let x and y be elements of EReal such that x ≠ ⊤ and y ≠ ⊤. Then their sum is not equal to ⊤.

Русский

Пусть x и y — элементы EReal и x ≠ ⊤, y ≠ ⊤. Тогда их сумма не равна ⊤.

LaTeX

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

Lean4

theorem add_ne_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y ≠ ⊤ :=
  lt_top_iff_ne_top.mp <| add_lt_top hx hy

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