English
The addition on EReal is continuous at points where at least one coordinate is not bottom or the other is not a problematic combination; in particular, at (⊥, a) and at (a, ⊥) for real a and at (⊤,⊤) and other combinations where defined.
Русский
Сложение в EReal непрерывно в точках, где хотя бы одна компонента не равна нижней границе или не возникает неопределённости; в частности, в точках (⊥, a) и (a, ⊥) для действительного a, а также в точках типа (⊤,⊤) и др.
LaTeX
$$$\\forall a\\in\\mathbb{R},\\; \\mathrm{ContinuousAt}\\bigl((x,y) \\mapsto x+y\\bigr)\\bigl((\\top)^{\\!\\mathrm{EReal}}, a^{\\!\\mathrm{EReal}}\\bigr) \\wedge \\mathrm{ContinuousAt}\\bigl((x,y) \\mapsto x+y\\bigr)\\bigl((a^{\\!\\mathrm{EReal}}, (\\top)^{\\!\\mathrm{EReal}})\\bigr)$$$
Lean4
theorem continuousAt_add_coe_coe (a b : ℝ) : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, b) := by
simp only [ContinuousAt, nhds_coe_coe, ← coe_add, tendsto_map'_iff, Function.comp_def, tendsto_coe, tendsto_add]
