English
The sigma-algebra generated by piiUnionInter of all measurable sets equals the supremum of the individual sigma-algebras m i over i ∈ S: generateFrom (piiUnionInter (λ n, {s | MeasurableSet[m n] s}) S) = ⨆ i ∈ S, m i.
Русский
Сигма-алгебра, порождаемая piiUnionInter из всех измеримых множеств, равна пересылке по сумме сигма-алгебр m i над i ∈ S.
LaTeX
$$$\mathrm{generateFrom}(\piiUnionInter(\lambda n, \{s \mid MeasurableSet[m n] s\}) S) = ⨆ i ∈ S, m i$$$
Lean4
theorem generateFrom_piiUnionInter_measurableSet (m : ι → MeasurableSpace α) (S : Set ι) :
generateFrom (piiUnionInter (fun n => {s | MeasurableSet[m n] s}) S) = ⨆ i ∈ S, m i :=
by
refine le_antisymm ?_ ?_
· rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]
exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)
· refine iSup₂_le fun i hi => ?_
rw [← @generateFrom_measurableSet α (m i)]
exact generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)
