iSup_generateFrom — Mathlib

English

The iSup over i of GenerateFrom(s i) equals GenerateFrom(Set.iUnion s i).

Русский

Объединение сверху по индексу i порождено как GenerateFrom множества, объединённого по i.

LaTeX

$$$\\iSup_{i} GenerateFrom(s(i)) = GenerateFrom(\\bigcup_{i} s(i))$$$

Lean4

theorem iSup_generateFrom (s : ι → Set (Set α)) : ⨆ i, generateFrom (s i) = generateFrom (⋃ i, s i) :=
  (@MeasurableSpace.giGenerateFrom α).gc.l_iSup.symm

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