English
Let t_i be a countable covering of a set T by measurable sets, and f_i : t_i → β be a family of functions that agree on overlaps. If T lies in the union of t_i and each t_i and f_i are measurable, then the lifted function iUnionLift t f is measurable.
Русский
Пусть t_i образуют счётное покрытие множества T измеримыми множествами, и для каждой i функция f_i : t_i → β согласуется на пересечениях. Если T ⊆ ⋃ i t_i, каждое t_i измеримо, и каждая f_i измерима, то функция iUnionLift t f измерима.
LaTeX
$$$[Countable \iota] \; (t : \iota → Set α) (f : \iota → (t_i) → β) \, (htf : \forall (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)) : \operatorname{Measurable}(\text{Set.iUnionLift } t f htf T hT)$$
Lean4
/-- A piecewise function on countably many pieces is measurable if all the data is measurable. -/
@[measurability]
theorem find {_ : MeasurableSpace α} {f : ℕ → α → β} {p : ℕ → α → Prop} [∀ n, DecidablePred (p n)]
(hf : ∀ n, Measurable (f n)) (hp : ∀ n, MeasurableSet {x | p n x}) (h : ∀ x, ∃ n, p n x) :
Measurable fun x => f (Nat.find (h x)) x :=
have : Measurable fun p : α × ℕ => f p.2 p.1 := measurable_from_prod_countable_left fun n => hf n
this.comp (Measurable.prodMk measurable_id (measurable_find h hp))
