setOf_isOpen_iSup — Mathlib

English

For a family t_i of topologies, a set s is open in the supremum topology ⨆ i t_i iff s is open in every t_i.

Русский

Для семейства топологий t_i множество s открыто в верхней вершине ⨆ i t_i тогда, когда s открыто во всех t_i.

LaTeX

$$$\\mathrm{IsOpen}[\\bigvee_i t_i]\,s \\iff \\forall i, \\mathrm{IsOpen}[t_i]\,s$$$

Lean4

theorem setOf_isOpen_iSup {t : ι → TopologicalSpace α} : {s | IsOpen[⨆ i, t i] s} = ⋂ i, {s | IsOpen[t i] s} :=
  (gc_generateFrom α).l_iSup

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