generateFrom_iUnion_isOpen — Mathlib

English

For f : ι → TopologicalSpace α, generateFrom(⋃ i, {s | IsOpen[f i] s}) = ⨅ i, f i.

Русский

Для f : ι → TopologicalSpace α, generateFrom(⋃ i, {s | IsOpen[f i] s}) = ⨅ i, f i.

LaTeX

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

Lean4

theorem generateFrom_iUnion_isOpen (f : ι → TopologicalSpace α) : generateFrom (⋃ i, {s | IsOpen[f i] s}) = ⨅ i, f i :=
  (gciGenerateFrom α).u_iInf_l _

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