generateFrom_sUnion — Mathlib

English

For S ⊆ Set(Set α), generateFrom(S.sUnion) equals the infimum over s ∈ S of generateFrom(s).

Русский

Для множества S ⊆ Set(Set α) порождаемая объединением S.sUnion топология равна infimum множества generateFrom(s) по s ∈ S.

LaTeX

$$$\\operatorname{generateFrom}(S^{\\sigma}) = \\bigwedge_{s \\in S} \\operatorname{generateFrom}(s)$$$

Lean4

theorem generateFrom_sUnion {S : Set (Set (Set α))} : generateFrom (⋃₀ S) = ⨅ s ∈ S, generateFrom s :=
  (gc_generateFrom α).u_sInf

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