closure_inter_coborder

Mathlib.Topology.LocallyClosed

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

English

The same symmetry as coborder_inter_closure: closure(s) ∩ coborder(s) = s.

Русский

Аналогично coborder_inter_closure: closure(s) ∩ coborder(s) = s.

LaTeX

$$$\overline{s} \cap \operatorname{coborder}(s) = s$$

Lean4

theorem closure_inter_coborder : closure s ∩ coborder s = s := by rw [inter_comm, coborder_inter_closure]

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

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

Разделы

Аффилиация

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