generateFrom_sup_generateFrom — Mathlib

English

The supremum of the generated sigma-algebras equals the generated sigma-algebra of the union: generateFrom s ⊔ generateFrom t = generateFrom (s ∪ t).

Русский

Наивысшее объединение порожденных сигма-алгебр равно порожденной сигма-алгебре от объединения: GenerateFrom s ⊔ GenerateFrom t = GenerateFrom(s ∪ t).

LaTeX

$$$\\operatorname{generateFrom}(s) \\sqcup \\operatorname{generateFrom}(t) = \\operatorname{generateFrom}(s \\cup t)$$$

Lean4

theorem generateFrom_sup_generateFrom {s t : Set (Set α)} : generateFrom s ⊔ generateFrom t = generateFrom (s ∪ t) :=
  (@giGenerateFrom α).gc.l_sup.symm

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