English
For any sets t and s in a topological space, t is contained in the interior of s if and only if there exists an open set U with t ⊆ U ⊆ s.
Русский
Для любых множеств t и s в топологическом пространстве: t ⊆ int(s) эквивалентно существованию открытого множества U с t ⊆ U ⊆ s.
LaTeX
$$$ \forall X [TopologicalSpace X], \forall s,t \subseteq X, t \subseteq \operatorname{int}(s) \iff \exists U, IsOpen(U) \land t \subseteq U \land U \subseteq s$$$
Lean4
theorem subset_interior_iff : t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s :=
⟨fun h => ⟨interior s, isOpen_interior, h, interior_subset⟩, fun ⟨_U, hU, htU, hUs⟩ =>
htU.trans (interior_maximal hUs hU)⟩
