setOf_isOpen_sSup — Mathlib

English

For T ⊆ Set(TopologicalSpace α), the open sets of sSup T are those s that are open in every t ∈ T.

Русский

Для T ⊆ Set(TopologicalSpace α) открытые множества s в sSup T являются открытыми во всех t ∈ T.

LaTeX

$$$\\{s \\mid \\mathrm{IsOpen}[sSup\,T]\,s\\} = \\bigcap_{t \\in T} \\{s \\mid \\mathrm{IsOpen}[t]\,s\\}$$$

Lean4

theorem setOf_isOpen_sSup {T : Set (TopologicalSpace α)} : {s | IsOpen[sSup T] s} = ⋂ t ∈ T, {s | IsOpen[t] s} :=
  (gc_generateFrom α).l_sSup

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