comap_gauge_nhds_zero — Mathlib

English

If s is balanced, convex, absorbent and s ∈ nhds 0, then comap (gauge s) (nhds 0) = nhds 0.

Русский

Если s сбалансировано, выпукло и абсорбирует, и s ∈ nhds(0), то comap (gauge s) (nhds 0) = nhds 0.

LaTeX

$$$$ \\operatorname{comap}(\\operatorname{gauge}(s))(\\mathcal{N}(0)) = \\mathcal{N}(0). $$$$

Lean4

theorem comap_gauge_nhds_zero (hb : Bornology.IsVonNBounded ℝ s) (h₀ : s ∈ 𝓝 0) : comap (gauge s) (𝓝 0) = 𝓝 0 :=
  (comap_gauge_nhds_zero_le (absorbent_nhds_zero h₀) hb).antisymm (tendsto_gauge_nhds_zero h₀).le_comap

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