α : Type ?u.27248
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.fst + a.snd < ↑x
α : Type ?u.27248
inst✝ : TopologicalSpace α
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
α : Type ?u.27248
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : x✝.fst < ↑0 ∧ x✝.snd < ↑r
⊢ x✝.fst + x✝.snd < ↑r
α : Type ?u.27248
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.fst + a.snd < ↑x
refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds
  (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_
no goals
α : Type ?u.27248
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : x✝.fst < ↑0 ∧ x✝.snd < ↑r
⊢ x✝.fst + x✝.snd < ↑r
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2