cthickening_closure

Mathlib.Topology.MetricSpace.Thickening

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

English

cthickening δ (closure E) = cthickening δ E.

Русский

cthickening δ (closure E) = cthickening δ E.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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