iff_neBot_and_le_nhds_one — Mathlib

English

In a topological unital magma, 𝓝 1 is the largest approximate unit.

Русский

В топологической монде с единицей 𝓝1 является наибольшей аппроксимационной единицей.

LaTeX

$$$$ [ContinuousMul \alpha] \{l : \text{Filter } \alpha\} \ \mathrm{IsApproximateUnit}(l) \Leftrightarrow (l.\mathrm{NeBot} \wedge l \le \mathcal{N}(1)). $$$$

Lean4

/-- In a topological unital magma, `𝓝 1` is the largest approximate unit. -/
theorem iff_neBot_and_le_nhds_one [ContinuousMul α] {l : Filter α} : IsApproximateUnit l ↔ l.NeBot ∧ l ≤ 𝓝 1 :=
  ⟨fun hl ↦ ⟨hl.neBot, by simpa using hl.tendsto_mul_left 1⟩, And.elim fun _ hl ↦ nhds_one α |>.mono hl⟩

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