isClosed_cthickening

Mathlib.Topology.MetricSpace.Thickening

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

← MathLib Explorer

English

For any δ and E, the closed thickening of E is a closed set.

Русский

Для любых δ и E замыкание утолщения E является замкнутым множеством.

LaTeX

$$IsClosed (cthickening δ E)$$

Lean4

/-- The closed thickening is a closed set. -/
theorem isClosed_cthickening {δ : ℝ} {E : Set α} : IsClosed (cthickening δ E) :=
  IsClosed.preimage continuous_infEdist isClosed_Iic

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

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

Разделы

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

Аффилиация

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