closure_subset_iff

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#IsClosed.closure_subset_iff

English

For a closed t, closure s ⊆ t iff s ⊆ t.

Русский

Для замкнутого t верно: closure s ⊆ t тогда и только тогда, когда s ⊆ t.

LaTeX

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

Lean4

theorem closure_subset_iff (h₁ : IsClosed t) : closure s ⊆ t ↔ s ⊆ t :=
  ⟨Subset.trans subset_closure, fun h => closure_minimal h h₁⟩

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

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

Разделы

Аффилиация

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