isOpen_sSup_iff — Mathlib

English

For s ⊆ α and T ⊆ TopologicalSpace α, s is open in sSup T iff for all t ∈ T, s is open in t.

Русский

Для s ⊆ α и T ⊆ TopologicalSpace α, s открыто в sSup T тогда и только тогда, когда для каждого t ∈ T, s открыто в t.

LaTeX

$$$\\mathrm{IsOpen}[sSup\,T]\,s \\iff \\forall t \\in T, \\mathrm{IsOpen}[t]\,s$$$

Lean4

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

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