English
For any S with x ∈ S, generateFrom (π x) ≤ generateFrom (piiUnionInter π S). The inclusion follows from subset_piiUnionInter.
Русский
Для любого S с x ∈ S выполняется generateFrom(π x) ≤ generateFrom(piiUnionInter π S). Следствие из subset_piiUnionInter.
LaTeX
$$$\forall x, x \in S \Rightarrow \mathrm{generateFrom}(\pi x) \le \mathrm{generateFrom}(\piiUnionInter(\pi) S)$$$
Lean4
theorem generateFrom_piiUnionInter_le {m : MeasurableSpace α} (π : ι → Set (Set α)) (h : ∀ n, generateFrom (π n) ≤ m)
(S : Set ι) : generateFrom (piiUnionInter π S) ≤ m :=
by
refine generateFrom_le ?_
rintro t ⟨ht_p, _, ft, hft_mem_pi, rfl⟩
refine Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ ?_
exact measurableSet_generateFrom (hft_mem_pi x hx_mem)
