generateFrom_union — Mathlib

English

Let f : ι → Set(Set α). The topology generated by the union of all f(i) equals the infimum of the generated topologies: generateFrom(⋃ i, f(i)) = ⨅ i, generateFrom(f(i)).

Русский

Пусть f : ι → Set(Set α). Топология, порождаемая объединением всех f(i), равна нижнему пределу порождаемых топологий: generateFrom(⋃ i, f(i)) = ⨅ i, generateFrom(f(i)).

LaTeX

$$$\\operatorname{generateFrom}\\left(\\bigcup_i f(i)\\right) = \\bigwedge_i \\operatorname{generateFrom}\\bigl(f(i)\\bigr)$$$

Lean4

theorem generateFrom_union (a₁ a₂ : Set (Set α)) : generateFrom (a₁ ∪ a₂) = generateFrom a₁ ⊓ generateFrom a₂ :=
  (gc_generateFrom α).u_inf

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