interior_union_inter_interior_compl_left_subset

English

The interior of the union, intersected with the complement of s, is contained in the interior of t: int(s ∪ t) ∩ int(s^c) ⊆ int(t).

Русский

Интерьер объединения, пересеченный с дополнением к s, принадлежит интерьеру t: int(s ∪ t) ∩ int(s^c) ⊆ int(t).

LaTeX

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

Lean4

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

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