frontier_subset_iff_isClosed

Mathlib.Topology.Closure

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

← MathLib Explorer

English

Frontier s ⊆ s is equivalent to IsClosed s.

Русский

Граница множества содержит множество ⇔ множество замкнуто.

LaTeX

$$$ frontier(s) \subseteq s \iff IsClosed(s) $$$

Lean4

theorem frontier_subset_iff_isClosed : frontier s ⊆ s ↔ IsClosed s := by
  rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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