English
The addition on EReal is continuous at every admissible point, i.e., whenever the sum is defined.
Русский
Сложение в EReal непрерывно во всех допустимых точках, где сумма определена.
LaTeX
$$$\\forall p\\in EReal\\times EReal,\\; \\text{defined}(p_1+p_2) \\Rightarrow \\mathrm{ContinuousAt}(\\lambda p, p_1+p_2)\\,p$$$
Lean4
/-- The addition on `EReal` is continuous except where it doesn't make sense (i.e., at `(⊥, ⊤)`
and at `(⊤, ⊥)`). -/
theorem continuousAt_add {p : EReal × EReal} (h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥) (h' : p.1 ≠ ⊥ ∨ p.2 ≠ ⊤) :
ContinuousAt (fun p : EReal × EReal => p.1 + p.2) p :=
by
rcases p with ⟨x, y⟩
induction x <;> induction y
· exact continuousAt_add_bot_bot
· exact continuousAt_add_bot_coe _
· simp at h'
· exact continuousAt_add_coe_bot _
· exact continuousAt_add_coe_coe _ _
· exact continuousAt_add_coe_top _
· simp at h
· exact continuousAt_add_top_coe _
· exact continuousAt_add_top_top
