interior_union_inter_interior_compl_right_subset

Mathlib.Topology.Closure

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

← MathLib Explorer

English

Dual statement: int(s ∪ t) ∩ int(t^c) ⊆ int(s).

Русский

Двойственная формула: int(s ∪ t) ∩ int(t^c) ⊆ int(s).

LaTeX

$$$ \operatorname{int}(s \cup t) \cap \operatorname{int}(t^{c}) \subseteq \operatorname{int}(s)$$$

Lean4

theorem interior_union_inter_interior_compl_right_subset : interior (s ∪ t) ∩ interior tᶜ ⊆ interior s :=
  interior_inter.symm.trans_subset <| interior_mono (union_inter_compl_right_subset ..)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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