nhds_one — Mathlib

English

In a topological unital magma, the neighborhood filter at 1 is an approximate unit.

Русский

В топологической моной с единицей окрестности единицы образуют аппроксимационную единицу.

LaTeX

$$$$ [\text{ContinuousMul } \alpha] \Rightarrow \mathrm{IsApproximateUnit}(\mathcal{N}(1)). $$$$

Lean4

/-- In a topological unital magma, `𝓝 1` is an approximate unit. -/
theorem nhds_one [ContinuousMul α] : IsApproximateUnit (𝓝 (1 : α))
    where
  tendsto_mul_left m := by simpa using tendsto_id (x := 𝓝 1) |>.const_mul m
  tendsto_mul_right m := by simpa using tendsto_id (x := 𝓝 1) |>.mul_const m

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