English
The addition on EReal is continuous at many points; in particular, for any a,b ∈ ℝ the map (p1,p2) ↦ p1+p2 is continuous at (a^E, b^E).
Русский
Сложение в EReal непрерывно в точках, в частности, при любых a,b ∈ ℝ отображение (p1,p2) ↦ p1+p2 непрерывно в точке (a^E, b^E).
LaTeX
$$$\\forall a,b \\in \\mathbb{R},\\; \\mathrm{ContinuousAt}\\bigl((x,y) \\mapsto x+y\\bigr)\\bigl(a^{\\!\\mathrm{EReal}}, b^{\\!\\mathrm{EReal}}\\bigr)$$$
Lean4
theorem liminf_mul_le [NeBot f] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) (h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤)
(h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0) : liminf (u * v) f ≤ limsup u f * liminf v f :=
by
replace h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤ :=
by
refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm
exact le_of_eq_of_le (limsup_const 0).symm (limsup_le_limsup hu)
replace h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f :=
by
refine h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm
exact le_of_eq_of_le (liminf_const 0).symm (liminf_le_liminf hv)
refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦ ?_
refine
(((frequently_lt_of_liminf_lt) b_v).and_eventually <| (eventually_lt_of_limsup_lt a_u).and <| hu.and hv).mono
fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab
