tendsto_gauge_nhds_zero

Mathlib.Analysis.Convex.Gauge

URI: https://scilib.ai/kg/mathlib#tendsto_gauge_nhds_zero

English

If s is a neighborhood of 0, then gauge s tends to 0 at 0 in the usual sense.

Русский

Если s окрестность 0, gauge s стремится к 0 в обычном смысле в точке 0.

LaTeX

$$$$ \\operatorname{Tendsto}(\\operatorname{gauge}(s))(\\mathcal{N}(0),\\mathcal{N}(0)). $$$$

Lean4

theorem tendsto_gauge_nhds_zero (hs : s ∈ 𝓝 0) : Tendsto (gauge s) (𝓝 0) (𝓝 0) :=
  (tendsto_gauge_nhds_zero_nhdsGE hs).mono_right inf_le_left

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru