isClosed_closedBall

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#EMetric.isClosed_closedBall

English

The set of LipschitzWith functions is closed in the appropriate function space.

Русский

Множество функций LipschitzWith замкнуто в пространстве функций.

LaTeX

$$$\text{IsClosed }\{f: \alpha \to \beta \mid \text{LipschitzWith } K\, f\}$.$$

Lean4

theorem isClosed_closedBall {a : α} {r : ℝ≥0∞} : IsClosed (closedBall a r) :=
  isClosed_le (continuous_id.edist continuous_const) continuous_const

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

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

Разделы

Аффилиация

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