isOpen_thickening

Mathlib.Topology.MetricSpace.Thickening

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

← MathLib Explorer

English

For any δ and E, the open thickening of E is an open set.

Русский

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

LaTeX

$$$IsOpen( thickening\\,δ\\,E )$$$

Lean4

/-- The (open) thickening is an open set. -/
theorem isOpen_thickening {δ : ℝ} {E : Set α} : IsOpen (thickening δ E) :=
  Continuous.isOpen_preimage continuous_infEdist _ isOpen_Iio

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

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

Разделы

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

Аффилиация

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