compQuasiMeasurePreserving_toGerm

English

If g is an ae-equivalent function on β, and f is quasi-measure-preserving, then composing g with f and taking its germ agrees with the germ composition on germs via tendsto.

Русский

Если g — ae-равна функция на β, а f — квази-измеримо-сохраняющая мера, то композиция г∘f и его га́рм согласуются с га́рмом при переходе через tendsto.

LaTeX

$$$(g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f hf.tendsto_ae$$$

Lean4

@[simp]
theorem compQuasiMeasurePreserving_toGerm {β : Type*} [MeasurableSpace β] {f : α → β} {ν} (g : β →ₘ[ν] γ)
    (hf : Measure.QuasiMeasurePreserving f μ ν) :
    (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f hf.tendsto_ae := by rcases g; rfl

Похожие утверждения