English
If g is a topological embedding, then f is strongly measurable iff g ∘ f is.
Русский
Если g — топологическое вложение, тогда f сильно измерим ⇔ g ∘ f сильно измерим.
LaTeX
$$$$\\text{StronglyMeasurable}(f) \\iff \\text{StronglyMeasurable}(g \\circ f).$$$$
Lean4
/-- If `g` is a topological embedding, then `f` is strongly measurable iff `g ∘ f` is. -/
theorem _root_.Embedding.comp_stronglyMeasurable_iff {m : MeasurableSpace α} [TopologicalSpace β]
[PseudoMetrizableSpace β] [TopologicalSpace γ] [PseudoMetrizableSpace γ] {g : β → γ} {f : α → β}
(hg : IsEmbedding g) : (StronglyMeasurable fun x => g (f x)) ↔ StronglyMeasurable f :=
by
letI := pseudoMetrizableSpacePseudoMetric γ
borelize β γ
refine
⟨fun H => stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩, fun H => hg.continuous.comp_stronglyMeasurable H⟩
· let G : β → range g := rangeFactorization g
have hG : IsClosedEmbedding G :=
{ hg.codRestrict _ _ with
isClosed_range := by
rw [rangeFactorization_surjective.range_eq]
exact isClosed_univ }
have : Measurable (G ∘ f) := Measurable.subtype_mk H.measurable
exact hG.measurableEmbedding.measurable_comp_iff.1 this
· have : IsSeparable (g ⁻¹' range (g ∘ f)) := hg.isSeparable_preimage H.isSeparable_range
rwa [range_comp, hg.injective.preimage_image] at this
