English
Let t_i be a nonempty countable covering of α by measurable sets, and g_i measurable with pairwise agreement on overlaps. Then there exists a measurable f: α → β that agrees with each g_i on t_i.
Русский
Пусть t_i образуют не пустое счётное покрытие α измеримыми множествами, и функции g_i : α → β измеримы и согласованы на пересечениях. Тогда существует измеримая функция f: α → β, которая совпадает с g_i на t_i для каждого i.
LaTeX
$$$\exists f: \alpha \to \beta,\; \operatorname{Measurable} f \land \forall i, \operatorname{EqOn} f (g i) (t i)$$$
Lean4
/-- Let `t i` be a nonempty countable family of measurable sets in `α`. Let `g i : α → β` be a
family of measurable functions such that `g i` agrees with `g j` on `t i ∩ t j`. Then there exists
a measurable function `f : α → β` that agrees with each `g i` on `t i`.
We only need the assumption `[Nonempty ι]` to prove `[Nonempty (α → β)]`. -/
theorem exists_measurable_piecewise {ι} [Countable ι] [Nonempty ι] (t : ι → Set α) (t_meas : ∀ n, MeasurableSet (t n))
(g : ι → α → β) (hg : ∀ n, Measurable (g n)) (ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)) :
∃ f : α → β, Measurable f ∧ ∀ n, EqOn f (g n) (t n) :=
by
inhabit ι
set g' : (i : ι) → t i → β := fun i =>
g i ∘
(↑)
-- see https://github.com/leanprover-community/mathlib4/issues/2184
have ht' : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩ :=
by
intro i j x hxi hxj
rcases eq_or_ne i j with rfl | hij
· rfl
· exact ht hij ⟨hxi, hxj⟩
set f : (⋃ i, t i) → β := iUnionLift t g' ht' _ Subset.rfl
have hfm : Measurable f := measurable_iUnionLift _ _ t_meas (fun i => (hg i).comp measurable_subtype_coe)
classical
refine
⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩
simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx
