generate_union — Mathlib

English

The filter generated by the union s ∪ t of collections equals the infimum of the generated filters: generate(s ∪ t) = generate(s) ⊓ generate(t).

Русский

Фильтр, порожденный объединением s ∪ t, равен инфимуму порожденных фильтров: generate(s ∪ t) = generate(s) ⊓ generate(t).

LaTeX

$$$\\operatorname{generate}(s \\cup t) = \\operatorname{generate}(s) \\sqcap \\operatorname{generate}(t)$$$

Lean4

theorem generate_union {s t : Set (Set α)} : Filter.generate (s ∪ t) = Filter.generate s ⊓ Filter.generate t :=
  (giGenerate α).gc.l_sup

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