English
If f is AEMeasurable and f(x) ∈ s for all x, then the restricted map to s given by codRestrict f s is AEMeasurable on μ.
Русский
Если f — AЕ-измеримая и f(x) ∈ s для всех x, тогда ограниченная карта на подмножество s через codRestrict f s является AЕ-измеримой на μ.
LaTeX
$$$\mathrm{AEMeasurable}(f, \mu) \rightarrow \forall s, (\forall x, f(x) \in s) \rightarrow \mathrm{AEMeasurable}(\mathrm{codRestrict}(f, s, \_), \mu)$$$
Lean4
theorem subtype_mk (h : AEMeasurable f μ) {s : Set β} {hfs : ∀ x, f x ∈ s} : AEMeasurable (codRestrict f s hfs) μ :=
by
nontriviality α; inhabit α
obtain ⟨g, g_meas, hg, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ s ∧ f =ᵐ[μ] g :=
h.exists_ae_eq_range_subset (Eventually.of_forall hfs) ⟨_, hfs default⟩
refine ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, ?_⟩
filter_upwards [fg] with x hx
simpa [Subtype.ext_iff]
