pure_one — Mathlib

English

If l is an approximate unit and l' ≤ l with l'.NeBot, then l' is also an approximate unit.

Русский

Если l является аппроксимационной единицей и l' ≤ l, причём l' не тривиален, то и l' является аппроксимационной единицей.

LaTeX

$$$$ \mathrm{IsApproximateUnit}(l) \wedge l' \le l \wedge l'.\mathrmNeBot \Rightarrow \mathrm{IsApproximateUnit}(l'). $$$$

Lean4

/-- A unital magma with a topology and bornology has the trivial approximate unit `pure 1`. -/
theorem pure_one : IsApproximateUnit (pure (1 : α))
    where
  tendsto_mul_left m := by simpa using tendsto_pure_nhds (m * ·) (1 : α)
  tendsto_mul_right m := by simpa using tendsto_pure_nhds (· * m) (1 : α)

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