closure_minimal

Mathlib.Topology.Closure

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

English

If s ⊆ t and t is closed, then closure s ⊆ t.

Русский

Если s ⊆ t и t замкнуто, то closure(s) ⊆ t.

LaTeX

$$(s \subseteq t) \land IsClosed t \Rightarrow \overline{s} \subseteq t$$

Lean4

theorem closure_minimal (h₁ : s ⊆ t) (h₂ : IsClosed t) : closure s ⊆ t :=
  sInter_subset_of_mem ⟨h₂, h₁⟩

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

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

Разделы

Аффилиация

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