English
If t_i form a countable covering of α by measurable sets and f_i : t_i → β are such that they agree on overlaps, then the global lift over the cover is measurable.
Русский
Если t_i образуют счётное покрытие α измеримыми множествами и f_i : t_i → β согласованы на пересечениях, то глобальная подстановка над покрытием измерима.
LaTeX
$$$[Countable\, \iota] \ (t : \iota → Set α) (htm : \forall i, MeasurableSet (t i)) (f : \iota → t i → β) (hfm : \forall i, Measurable (f i)) (hf : \forall (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x,hxi⟩ = f j ⟨x,hxj⟩) (htU : ⋃ i, t i = \; \!\! univ) : \operatorname{Measurable}(\text{liftCover } t f hf htU)$$$
Lean4
/-- Let `t i` be a countable covering of `α` 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.liftCover t f _ _`,
defined as `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable. -/
theorem measurable_liftCover [Countable ι] (t : ι → Set α) (htm : ∀ i, MeasurableSet (t i)) (f : ∀ i, t i → β)
(hfm : ∀ i, Measurable (f i)) (hf : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩)
(htU : ⋃ i, t i = univ) : Measurable (liftCover t f hf htU) := fun s hs =>
by
rw [preimage_liftCover]
exact .iUnion fun i => .subtype_image (htm i) <| hfm i hs
