English
For all x,y in EReal, if x ≠ ⊥ and y ≠ ⊥, then x+y ≠ ⊤ is equivalent to x ≠ ⊤ and y ≠ ⊤.
Русский
Для всех x,y ∈ EReal, если x ≠ ⊥ и y ≠ ⊥, то x+y ≠ ⊤ эквивалентно x ≠ ⊤ и y ≠ ⊤.
LaTeX
$$$$\forall x,y\in \mathrm{EReal},\ (x \neq \bot \land y \neq \bot) \Rightarrow \big( x+y \neq \top \iff (x \neq \top \land y \neq \top) \big).$$$$
Lean4
theorem add_ne_top_iff_ne_top₂ {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤ :=
by
refine ⟨?_, fun h ↦ add_ne_top h.1 h.2⟩
cases x <;> simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false, IsEmpty.forall_iff]
cases y <;>
simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false, coe_ne_top, and_self, implies_true]
