Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.Kernel.AEFiniteKernelSupport.comap_equiv

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:765 to 776

Mathematical statement

Exact Lean statement

lemma AEFiniteKernelSupport.comap_equiv [Countable U] [MeasurableSingletonClass U]
  {κ : Kernel T S} {μ : Measure T}
    (hκ : AEFiniteKernelSupport κ μ) (f : U ≃ᵐ T) :
    AEFiniteKernelSupport (Kernel.comap κ f f.measurable) (μ.comap f)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma AEFiniteKernelSupport.comap_equiv [Countable U] [MeasurableSingletonClass U]  {κ : Kernel T S} {μ : Measure T}    (hκ : AEFiniteKernelSupport κ μ) (f : U ≃ᵐ T) :    AEFiniteKernelSupport (Kernel.comap κ f f.measurable) (μ.comap f) := by  rw [← @MeasurableEquiv.map_symm]  rw [AEFiniteKernelSupport]  simp_rw [Kernel.comap_apply]  rw [ae_map_iff f.symm.measurable.aemeasurable]  · simp only [MeasurableEquiv.apply_symm_apply]    exact hκ  · rw [Set.setOf_exists]    measurability