English
In a second-countable setting, the first coordinate in an identically distributed pair is ae-strongly measurable.
Русский
Вторая счетная топология — первая координата в паре с идентичным распределением есть ae-сложно измеримая.
LaTeX
$$$[TopologicalSpace γ] [PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] [SecondCountableTopology γ] (h : IdentDistrib f g μ ν) : AEStronglyMeasurable f μ$$$
Lean4
/-- In a second countable topology, the first function in an identically distributed pair is a.e.
strongly measurable. So is the second function, but use `h.symm.aestronglyMeasurable_fst` as
`h.aestronglyMeasurable_snd` has a different meaning. -/
theorem aestronglyMeasurable_fst [TopologicalSpace γ] [PseudoMetrizableSpace γ] [OpensMeasurableSpace γ]
[SecondCountableTopology γ] (h : IdentDistrib f g μ ν) : AEStronglyMeasurable f μ :=
h.aemeasurable_fst.aestronglyMeasurable
