cthickening_zero

Mathlib.Topology.MetricSpace.Thickening

URI: https://scilib.ai/kg/mathlib#Metric.cthickening_zero

← MathLib Explorer

English

The closed thickening with radius zero is the closure of the set: cthickening 0 E = closure E.

Русский

Утолщение с радиусом ноль равно замыканию множества: cthickening 0 E = closure E.

LaTeX

$$$ cthickening 0 E = closure E $$$

Lean4

/-- The closed thickening with radius zero is the closure of the set. -/
@[simp]
theorem cthickening_zero (E : Set α) : cthickening 0 E = closure E :=
  cthickening_of_nonpos le_rfl E

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

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

Разделы

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

Аффилиация

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