tendsto_gauge_nhds_zero_nhdsGE — Mathlib

English

If s is a neighborhood of the origin, then gauge s tends to 0 along the nhds of 0, and even tends within the nonnegative ray.

Русский

Если s является окрестностью нуля, gauge s стремится к 0 по nhds(0) и далее к лучу неотрицательных значений.

LaTeX

$$$$ \\text{Tendsto}(\\operatorname{gauge}(s),\\ nhds(0),\\ nhdsWithin(0,(\\mathsf{Ici}0))). $$$$

Lean4

theorem tendsto_gauge_nhds_zero_nhdsGE (hs : s ∈ 𝓝 0) : Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0) :=
  by
  refine nhdsGE_basis_Icc.tendsto_right_iff.2 fun ε hε ↦ ?_
  rw [← set_smul_mem_nhds_zero_iff hε.ne'] at hs
  filter_upwards [hs] with x hx
  exact ⟨gauge_nonneg _, gauge_le_of_mem hε.le hx⟩

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