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

ProbabilityTheory.Kernel.FiniteSupport.comap_equiv

PFR.ForMathlib.Entropy.Kernel.Basic · PFR/ForMathlib/Entropy/Kernel/Basic.lean:175 to 188

Mathematical statement

Exact Lean statement

lemma FiniteSupport.comap_equiv [MeasurableSingletonClass T]
    {T' : Type*} [MeasurableSpace T']
    {μ : Measure T} (f : T' ≃ᵐ T) [FiniteSupport μ] :
    FiniteSupport (μ.comap f)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma FiniteSupport.comap_equiv [MeasurableSingletonClass T]    {T' : Type*} [MeasurableSpace T']    {μ : Measure T} (f : T' ≃ᵐ T) [FiniteSupport μ] :    FiniteSupport (μ.comap f) := by  classical  let A := μ.support  have hA := measure_compl_support μ  refine ⟨Finset.image f.symm A, ?_⟩  change (Measure.comap (⇑f) μ) (A.image f.symm)ᶜ = 0  rwa [Finset.coe_image, ← Set.image_compl_eq (MeasurableEquiv.bijective f.symm),    Measure.comap_apply f (MeasurableEquiv.injective f),MeasurableEquiv.image_symm,    MeasurableEquiv.image_preimage]  · exact fun _ ↦ (MeasurableEquiv.measurableSet_image f).mpr  · exact f.symm.measurableSet_image.mpr A.measurableSet.compl