iff_le_nhds_one — Mathlib

English

In a topological unital magma, an l is an approximate unit iff l ≤ 𝓝 1 (assuming l ≠ ⊥).

Русский

В топологической моноде с единицей аппроксимационная единица существует тогда и только тогда, когда l ≤ 𝓝(1) (при условии l ≠ ⊥).

LaTeX

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

Lean4

/-- In a topological unital magma, `𝓝 1` is the largest approximate unit. -/
theorem iff_le_nhds_one [ContinuousMul α] {l : Filter α} [l.NeBot] : IsApproximateUnit l ↔ l ≤ 𝓝 1 := by
  simpa [iff_neBot_and_le_nhds_one] using fun _ ↦ ‹_›

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