interior_subset_iff — Mathlib

English

The interior of s is contained in t if and only if every open set contained in s is contained in t.

Русский

interior(s) ⊆ t эквивалентно тому, что для каждого открытого множества U, если U ⊆ s, то U ⊆ t.

LaTeX

$$$ \operatorname{int}(s) \subseteq t \iff \forall U, \ IsOpen(U) \rightarrow U \subseteq s \rightarrow U \subseteq t$$$

Lean4

theorem interior_subset_iff : interior s ⊆ t ↔ ∀ U, IsOpen U → U ⊆ s → U ⊆ t := by simp [interior]

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