mul_const — Mathlib

English

The product of neighborhoods is contained in the neighborhood of the product: nhds a · nhds b ≤ nhds(ab).

Русский

Произведение окрестностей содержится в окрестности произведения: nhds a · nhds b ≤ nhds(ab).

LaTeX

$$$\nhds a \cdot \nhds b \leq \nhds(a b)$$$

Lean4

@[to_additive]
theorem mul_const (b : M) {c : M} {f : α → M} {l : Filter α} (h : Tendsto (fun k : α => f k) l (𝓝 c)) :
    Tendsto (fun k : α => f k * b) l (𝓝 (c * b)) :=
  h.mul tendsto_const_nhds

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