generate_iUnion — Mathlib

English

Let (s_i) be a family of collections of subsets of α, indexed by i in ι. Then the filter generated by the union of all s_i equals the greatest lower bound of the filters generated by each s_i:

Русский

Пусть для множества α дано семейство коллекций подмножеств s_i, индексируемое по i ∈ ι. Тогда фильтр, порожденный объединением ⋃_i s_i, равен наибольшей нижней границе фильтров, порожденных каждым s_i:

LaTeX

$$$\operatorname{generate}\left(\bigcup_{i} s_i\right) = \bigwedge_{i} \operatorname{generate}(s_i)$$$

Lean4

theorem generate_iUnion {s : ι → Set (Set α)} : Filter.generate (⋃ i, s i) = ⨅ i, Filter.generate (s i) :=
  (giGenerate α).gc.l_iSup

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