English
If u and v are nonnegative along a filter f with NeBot, then liminf(u·v) ≤ limsup u · liminf v.
Русский
Если u и v неотрицательны вдоль фильтра f и f не тривиален, то liminf(u·v) ≤ limsup u · liminf v.
LaTeX
$$$[\\text{NeBot } f] \\;\\mathrm{EventualLE}\\ 0\\ u\\to \\; \\mathrm{EventualLE}\\ 0\\ v \\Rightarrow \\liminf_f (u v) \\le \\limsup_f u \\cdot \\liminf_f v$$
Lean4
/-- The multiplication on `EReal` is continuous except at indeterminacies
(i.e. whenever one value is zero and the other infinite). -/
theorem continuousAt_mul {p : EReal × EReal} (h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥) (h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤) (h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0)
(h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0) : ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) p :=
by
rcases p with ⟨x, y⟩
induction x <;> induction y
· exact continuousAt_mul_symm3 continuousAt_mul_top_top
· simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃
exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)
· exact EReal.neg_top ▸ continuousAt_mul_symm1 continuousAt_mul_top_top
· simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁
exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))
· exact continuousAt_mul_coe_coe _ _
· simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂
exact continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)
· exact continuousAt_mul_symm2 continuousAt_mul_top_top
· simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄
exact continuousAt_mul_top_ne_zero h₄
· exact continuousAt_mul_top_top
