subset_interior_iff — Mathlib

English

Let S be an open subset of a topological space X. Then S is contained in the interior of T if and only if S is contained in T.

Русский

Пусть S — открытое подмножество топологического пространства X. Тогда S ⊆ int(T) тогда и только тогда, когда S ⊆ T.

LaTeX

$$$ \forall X [TopologicalSpace X], \forall s,t \subseteq X, IsOpen(s) \Rightarrow \left( s \subseteq \operatorname{int}(t) \iff s \subseteq t \right)$$$

Lean4

theorem subset_interior_iff (h₁ : IsOpen s) : s ⊆ interior t ↔ s ⊆ t :=
  ⟨fun h => Subset.trans h interior_subset, fun h₂ => interior_maximal h₂ h₁⟩

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