isClosed_sSup_iff

Mathlib.Topology.Order

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

← MathLib Explorer

English

For s ⊆ α and T ⊆ TopologicalSpace α, IsClosed[sSup T] s iff ∀ t ∈ T, IsClosed t s.

Русский

Для s и T, IsClosed[sSup T] s эквивалентно ∀ t ∈ T, IsClosed t s.

LaTeX

$$$IsClosed[sSup T] s \\iff \\forall t \\in T, IsClosed t s$$$

Lean4

theorem isClosed_sSup_iff {s : Set α} {T : Set (TopologicalSpace α)} : IsClosed[sSup T] s ↔ ∀ t ∈ T, IsClosed[t] s := by
  simp only [sSup_eq_iSup, isClosed_iSup_iff]

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

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

Разделы

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

Аффилиация

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