English
For any s: ι → Set α and S, the sigma-algebra generated by the singleton-intersection family equals the sigma-algebra generated by the sets s(i) with i ∈ S, i.e., generateFrom(piiUnionInter(λ i, {s(i)}) S) = generateFrom { t | ∃ i ∈ S, s(i) = t }.
Русский
Для функций s и множества S, образующаяся сигма-алгебра, порождаемая семейством одиночных множеств {s(i)} над S, равна порождаемой сигма-алгеброй множеств {s(i) : i ∈ S}.
LaTeX
$$$\mathrm{generateFrom}(\piiUnionInter(\lambda i, \{s(i)\}) S) = \mathrm{generateFrom}\{ t \mid ∃ i ∈ S, s(i) = t \}$$$
Lean4
theorem generateFrom_piiUnionInter_singleton_left (s : ι → Set α) (S : Set ι) :
generateFrom (piiUnionInter (fun k => {s k}) S) = generateFrom {t | ∃ k ∈ S, s k = t} :=
by
refine le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)
· rintro _ ⟨I, hI, f, hf, rfl⟩
refine Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom ?_
exact ⟨m, hI hm, (hf m hm).symm⟩
· rintro _ ⟨k, hk, rfl⟩
refine ⟨{ k }, fun m hm => ?_, s, fun i _ => ?_, ?_⟩
· rw [Finset.mem_coe, Finset.mem_singleton] at hm
rwa [hm]
· exact Set.mem_singleton _
· simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]
