English
If f is strongly measurable on subspaces whose union covers the whole space, then f is strongly measurable on the whole space.
Русский
Если f сильно измерима на подпространствах, чьи объединения покрывают всю пространство, то f сильно измерима на всей области.
LaTeX
$$$\forall s,t, \ MeasurableSet(s) \,\land\, \ MeasurableSet(t) \land \, univ \subseteq s \cup t \Rightarrow (f|_s, f|_t) \,\Rightarrow \mathrm{StronglyMeasurable}(f)$$$
Lean4
theorem _root_.stronglyMeasurable_of_stronglyMeasurable_union_cover {m : MeasurableSpace α} [TopologicalSpace β]
{f : α → β} (s t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t) (h : univ ⊆ s ∪ t)
(hc : StronglyMeasurable fun a : s => f a) (hd : StronglyMeasurable fun a : t => f a) : StronglyMeasurable f :=
by
nontriviality β; inhabit β
suffices Function.extend Subtype.val (fun x : s ↦ f x) (Function.extend (↑) (fun x : t ↦ f x) fun _ ↦ default) = f
from
this ▸ (MeasurableEmbedding.subtype_coe hs).stronglyMeasurable_extend hc <|
(MeasurableEmbedding.subtype_coe ht).stronglyMeasurable_extend hd stronglyMeasurable_const
ext x
by_cases hxs : x ∈ s
· lift x to s using hxs
simp
· lift x to t using (h trivial).resolve_left hxs
rw [extend_apply', Subtype.coe_injective.extend_apply]
exact fun ⟨y, hy⟩ ↦ hxs <| hy ▸ y.2
