English
If a limit holds for right multiplication by every m with 0 ≤ m and ||m|| < 1, then it holds for left multiplication as well.
Русский
Если предел для правого умножения выполняется для каждого m с 0 ≤ m и ||m|| < 1, то аналогично сохраняется и для левого умножения.
LaTeX
$$$$ (\forall m, 0 \le m \land \|m\| < 1 \Rightarrow \mathrm{Tendsto}(x \mapsto x m) l (\mathcal N m)) \Rightarrow (\forall m, \mathrm{Tendsto}(x \mapsto m x) l (\mathcal N m)) $$$$
Lean4
/-- To show that `l` is a one-sided approximate unit for `A`, it suffices to verify it only for
`m : A` with `0 ≤ m` and `‖m‖ < 1`. -/
theorem tendsto_mul_right_of_forall_nonneg_tendsto {l : Filter A} (h : ∀ m, 0 ≤ m → ‖m‖ < 1 → Tendsto (· * m) l (𝓝 m))
(m : A) : Tendsto (· * m) l (𝓝 m) :=
by
obtain ⟨n, c, x, rfl⟩ :=
mem_span_set'.mp <| by
change m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)
simp [span_nonneg_inter_unitBall]
simp_rw [Finset.mul_sum]
refine tendsto_finset_sum _ fun i _ ↦ ?_
simp_rw [mul_smul_comm]
exact tendsto_const_nhds.smul <| h (x i) (x i).2.1 <| by simpa using (x i).2.2
