generateFrom_iInter_of_generateFrom_eq_self

English

If for all i we have {s | IsOpen[generateFrom (f i)] s} = f i, then generateFrom (⋂ i, f i) = ⨆ i, generateFrom (f i).

Русский

Если для каждого i верно {s | IsOpen[generateFrom (f i)] s} = f i, то generateFrom(⋂ i, f i) = ⨆ i, generateFrom(f i).

LaTeX

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

Lean4

theorem generateFrom_iInter_of_generateFrom_eq_self (f : ι → Set (Set α))
    (hf : ∀ i, {s | IsOpen[generateFrom (f i)] s} = f i) : generateFrom (⋂ i, f i) = ⨆ i, generateFrom (f i) :=
  (gciGenerateFrom α).u_iSup_of_lu_eq_self f hf

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