Theorems · Theorem · probability

ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul

∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X},
  𝓑 ≤ 𝓧 →
    (π.IsProper ↔
      ∀ ⦃A : Set X⦄,
        MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A)

Defined in: Mathlib.Probability.Kernel.Proper
Cited by: 2 results in Mathlib
Foundations: Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
MeasurableSetstatement and proof · cited by 3,075
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
Set.indicatorstatement and proof · cited by 723
MeasureTheory.Measure.restrict_applyproof · cited by 159
ProbabilityTheory.Kernel.restrictproof · cited by 19
ProbabilityTheory.Kernel.IsProperstatement · cited by 11
ProbabilityTheory.Kernel.restrict_applyproof · cited by 9

Cited by2

Results whose statement or proof uses this declaration.

ProbabilityTheory.Kernel.IsProper.inter_eq_indicator_mulproof · cited by 1
ProbabilityTheory.Kernel.IsProper.of_inter_eq_indicator_mulproof · cited by 0