compMeasurable_toGerm — Mathlib

English

If g is measurable and f is AE-measurable, then compMeasurable g hg f has germ equal to f’s germ mapped by g.

Русский

Если g измеримо и f AE-измерима, то га́рм compMeasurable равен га́рму f, отображённому через g.

LaTeX

$$$compMeasurable\ g\ hg\ f.toGerm = f.toGerm.map g$$$

Lean4

theorem compMeasurable_toGerm [MeasurableSpace β] [BorelSpace β] [PseudoMetrizableSpace β] [PseudoMetrizableSpace γ]
    [SecondCountableTopology γ] [MeasurableSpace γ] [OpensMeasurableSpace γ] (g : β → γ) (hg : Measurable g)
    (f : α →ₘ[μ] β) : (compMeasurable g hg f).toGerm = f.toGerm.map g :=
  induction_on f fun f _ => by simp

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