English
For any real a, the map (p1,p2) ↦ p1+p2 is continuous at the point (top, a) in EReal × EReal.
Русский
Для любого действительного a отображение (p1,p2) ↦ p1+p2 непрерывно в точке (верхняя граница, a) в пространстве EReal × EReal.
LaTeX
$$$\\forall a\\in\\mathbb{R},\\; \\mathrm{ContinuousAt}\\bigl((x,y) \\mapsto x+y\\bigr)\\bigl( (\\top)^{\\!\\mathrm{EReal}}, a^{\\!\\mathrm{EReal}} \\bigr)$$$
Lean4
theorem continuousAt_add_top_coe (a : ℝ) : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊤, a) :=
by
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]
refine fun r ↦
((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono
fun _ h ↦ ?_
simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2
