English
For ENNReal, if ma → a and mb → b along f, with not both a ≠ 0 and b ≠ ∞, then ma a · mb a → a · b.
Русский
Для ENNReal, если ma → a и mb → b вдоль f, при условии, что не выполняются оба a = 0 и b = ∞, то ma a · mb a → a · b.
LaTeX
$$$\\\\forall {f: Filter α} {ma mb: α → ENNReal} {a b : ENNReal}, \\\\ Tendsto ma f (\\\\nhds a) \\\\Rightarrow \\\\text{(not both degenerate)} \\\\Rightarrow \\\\ Tendsto mb f (\\\\nhds b) \\\\Rightarrow \\\\text{Tendsto } (\\\\lambda a, ma a * mb a) f (\\\\nhds (a * b)).$$$
Lean4
protected theorem tendsto_mul (ha : a ≠ 0 ∨ b ≠ ∞) (hb : b ≠ 0 ∨ a ≠ ∞) :
Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b)) :=
by
have ht : ∀ b : ℝ≥0∞, b ≠ 0 → Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞) := fun b hb =>
by
refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_
rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩
have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
(lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
refine this.mono fun c hc => ?_
exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)
induction a with
| top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb]
| coe a =>
induction b with
| top =>
simp only [ne_eq, or_false, not_true_eq_false] at ha
simpa [Function.comp_def, mul_comm, mul_top ha] using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
| coe b => simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def, tendsto_mul]
