English
Let f be a function between measurable and topological spaces. Then f is strongly measurable if and only if f is measurable and the range of f is separable.
Русский
Пусть f: α → β. Тогда f сильно измерима тогда и только тогда, когда она измерима и образ f(α) сепарабелен.
LaTeX
$$$\mathrm{StronglyMeasurable}(f) \iff \mathrm{Measurable}(f) \land \mathrm{IsSeparable}(\mathrm{range}(f))$$$
Lean4
/-- A function is strongly measurable if and only if it is measurable and has separable
range. -/
theorem _root_.stronglyMeasurable_iff_measurable_separable {m : MeasurableSpace α} [TopologicalSpace β]
[PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] :
StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f) :=
by
refine ⟨fun H ↦ ⟨H.measurable, H.isSeparable_range⟩, fun ⟨Hm, Hsep⟩ ↦ ?_⟩
have := Hsep.secondCountableTopology
have Hm' : StronglyMeasurable (rangeFactorization f) := Hm.subtype_mk.stronglyMeasurable
exact continuous_subtype_val.comp_stronglyMeasurable Hm'
