interior_compl

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#interior_compl

English

Interior of the complement equals the complement of the closure: int(sᶜ) = (cl s)ᶜ.

Русский

Внутренность дополнения равна дополнению замыкания: int(sᶜ) = (cl s)ᶜ.

LaTeX

$$$\\\\operatorname{int}(s^c) = (\\\\overline{s})^c$$$

Lean4

@[simp]
theorem interior_compl : interior sᶜ = (closure s)ᶜ := by simp [closure_eq_compl_interior_compl]

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

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

Разделы

Аффилиация

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