uniformContinuous_gauge

Mathlib.Analysis.Convex.Gauge

URI: https://scilib.ai/kg/mathlib#Convex.uniformContinuous_gauge

← MathLib Explorer

English

If s is convex and nhds(0) ⊆ s, then gauge s is uniformly continuous.

Русский

Если s выпуклоe и nhds(0) ⊆ s, то gauge s является равномерно непрерывной.

LaTeX

$$$$ \mathrm{UniformContinuous}(\mathrm{gauge}(s)). $$$$

Lean4

theorem uniformContinuous_gauge (hc : Convex ℝ s) (h₀ : s ∈ 𝓝 (0 : E)) : UniformContinuous (gauge s) :=
  let ⟨_K, hK⟩ := hc.lipschitz_gauge h₀;
  hK.uniformContinuous

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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