interior_eq_compl_closure_compl

Mathlib.Topology.Closure

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

English

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

Русский

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

LaTeX

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

Lean4

theorem interior_eq_compl_closure_compl : interior s = (closure sᶜ)ᶜ := by simp

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

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

Разделы

Аффилиация

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