thickening_closure

Mathlib.Topology.MetricSpace.Thickening

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

English

Closed thickening commutes with closure: cthickening δ (closure E) = cthickening δ E.

Русский

Закрытое утолщение коммутирует с замыканием: cthickening δ (closure E) = cthickening δ E.

LaTeX

$$$\\mathrm{cthickening}_{\\delta}(\\overline{E}) = \\mathrm{cthickening}_{\\delta}(E).$$$

Lean4

@[simp]
theorem thickening_closure : thickening δ (closure s) = thickening δ s := by simp_rw [thickening, infEdist_closure]

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

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

Разделы

Аффилиация

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