le_nhds_mul — Mathlib

English

For a topological monoid M with continuous multiplication, the product of neighborhood filters tightens to the neighborhood of the product: 𝓝 a · 𝓝 b ≤ 𝓝(ab).

Русский

Для топологического моноида M с непрерывным умножением произведение фильтров окрестностей удовлетворяет 𝓝 a · 𝓝 b ≤ 𝓝(ab).

LaTeX

$$$\mathcal{N}(a) \cdot \mathcal{N}(b) \leq \mathcal{N}(ab)$$$

Lean4

@[to_additive]
theorem le_nhds_mul (a b : M) : 𝓝 a * 𝓝 b ≤ 𝓝 (a * b) :=
  by
  rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]
  exact continuous_mul.tendsto _

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