English
In spaces with second-countable topology, measurable implies strongly measurable.
Русский
В пространствах со вторым счетным топологическим основанием измеримость влечет за собой сильную измеримость.
LaTeX
$$$\forall f: \alpha \to β, \text{Measurable } f \Rightarrow \text{StronglyMeasurable } f$$$
Lean4
/-- In a space with second countable topology, measurable implies strongly measurable. -/
@[aesop 90% apply (rule_sets := [Measurable])]
theorem _root_.Measurable.stronglyMeasurable [TopologicalSpace β] [PseudoMetrizableSpace β] [SecondCountableTopology β]
[OpensMeasurableSpace β] (hf : Measurable f) : StronglyMeasurable f :=
by
letI := pseudoMetrizableSpacePseudoMetric β
nontriviality β; inhabit β
exact
⟨SimpleFunc.approxOn f hf Set.univ default (Set.mem_univ _), fun x ↦
SimpleFunc.tendsto_approxOn hf (Set.mem_univ _) (by simp)⟩
