English
Let t_i be a countable family of sets with T ⊆ ⋃ t_i and compatible f_i : t_i → β. If each t_i is measurable and each f_i is measurable, then Set.iUnionLift t f is measurable.
Русский
Пусть t_i образуют счётное семейство множеств с T ⊆ ⋃ t_i и совместимыми f_i : t_i → β. Тогда Set.iUnionLift t f измеримо, если каждое t_i измеримо и каждый f_i измерим.
LaTeX
$$$[Countable\, \iota] \ {t : \iota → Set α} {f : (i : \iota) → (t i) → β} (htm : \forall i, MeasurableSet (t i)) (hfm : \forall i, Measurable (f i)) : \operatorname{Measurable}(\text{Set.iUnionLift } t f htf T hT)$$$
Lean4
/-- Let `t i` be a countable covering of a set `T` by measurable sets. Let `f i : t i → β` be a
family of functions that agree on the intersections `t i ∩ t j`. Then the function
`Set.iUnionLift t f _ _ : T → β`, defined as `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable. -/
theorem measurable_iUnionLift [Countable ι] {t : ι → Set α} {f : ∀ i, t i → β}
(htf : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) {T : Set α} (hT : T ⊆ ⋃ i, t i)
(htm : ∀ i, MeasurableSet (t i)) (hfm : ∀ i, Measurable (f i)) : Measurable (iUnionLift t f htf T hT) := fun s hs =>
by
rw [preimage_iUnionLift]
exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)
