generateFrom_iInter — Mathlib

English

For a family f: ι → TopologicalSpace α, generateFrom(⋂ i, {s | IsOpen[f i] s}) = ⨆ i, f i.

Русский

Для семейства f: ι → TopologicalSpace α порождаемая через пересечение открытых множеств f(i) равна супремуму TopologicalSpace f(i).

LaTeX

$$$\\operatorname{generateFrom}\\left(\\bigcap_i \\{s \\mid \\mathrm{IsOpen}[f(i)]\,s\\}\\right) = \\bigvee_i f(i)$$$

Lean4

theorem generateFrom_iInter (f : ι → TopologicalSpace α) : generateFrom (⋂ i, {s | IsOpen[f i] s}) = ⨆ i, f i :=
  (gciGenerateFrom α).u_iSup_l _

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