subset_interior_union — Mathlib

English

The interior of the union contains the union of interiors: int(s) ∪ int(t) ⊆ int(s ∪ t).

Русский

Интерьер объединения содержит объединение интерьеров: int(s) ∪ int(t) ⊆ int(s ∪ t).

LaTeX

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

Lean4

theorem subset_interior_union : interior s ∪ interior t ⊆ interior (s ∪ t) :=
  union_subset (interior_mono subset_union_left) (interior_mono subset_union_right)

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