tendsto_mul — Mathlib

English

The map (a,b) ↦ a b from M × M to M is continuous; equivalently, Tendsto (p ↦ p.fst p.snd) (nhds(a,b)) (nhds(a b)).

Русский

Отображение умножения $(a,b) \mapsto a b$ непрерывно; т.е. предел идёт к произведению.

LaTeX

$$$\text{ContinuousMul}$: \text{Tendsto}( (a,b) \mapsto a b,\; \nhds(a,b),\; \nhds(a b) )$$

Lean4

@[to_additive]
theorem tendsto_mul {a b : M} : Tendsto (fun p : M × M => p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b)) :=
  continuous_iff_continuousAt.mp ContinuousMul.continuous_mul (a, b)

Похожие утверждения