Theorems · Definition · probability

ProbabilityTheory.Kernel.comapRight

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} →
            {f : γ → β} → ProbabilityTheory.Kernel α β → MeasurableEmbedding f → ProbabilityTheory.Kernel α γ

Kernel with value (κ a).comap f, for a measurable embedding f. That is, for a measurable set t : Set β, ProbabilityTheory.Kernel.comapRight κ hf a t = κ a (f '' t).

Defined in

Mathlib.Probability.Kernel.Basic

Cited by

8 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound