interior_maximal

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#interior_maximal

English

If t ⊆ s and t is open, then t ⊆ interior(s).

Русский

Если t ⊆ s и t открыто, то t ⊆ interior(s).

LaTeX

$$$$ t \subseteq \operatorname{interior}(s) $$$$

Lean4

theorem interior_maximal (h₁ : t ⊆ s) (h₂ : IsOpen t) : t ⊆ interior s :=
  subset_sUnion_of_mem ⟨h₂, h₁⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru