English
If t is in piiUnionInter (λ n, {s | MeasurableSet[m n] s}) S, then t is measurable with respect to the supremum of m over S, i.e., t ∈ MeasurableSet[⨆ i ∈ S, m i] t.
Русский
Если t принадлежит piiUnionInter (λ n, {s | MeasurableSet[m n] s}) S, то t измеримо относительно суммарной сверхмножества m над S.
LaTeX
$$$\text{ht} \in piiUnionInter(\lambda n, \{s \mid MeasurableSet[m n] s\}) S \Rightarrow t \in MeasurableSet[\bigvee_{i \in S} m i] t$$$
Lean4
theorem measurableSet_iSup_of_mem_piiUnionInter (m : ι → MeasurableSpace α) (S : Set ι) (t : Set α)
(ht : t ∈ piiUnionInter (fun n => {s | MeasurableSet[m n] s}) S) : MeasurableSet[⨆ i ∈ S, m i] t :=
by
rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩
refine pt.measurableSet_biInter fun i hi => ?_
suffices h_le : m i ≤ ⨆ i ∈ S, m i from h_le (ft i) (ht_m i hi)
have hi' : i ∈ S := hpt hi
exact le_iSup₂ (f := fun i (_ : i ∈ S) => m i) i hi'
