CompNotation

📁 Source: Mathlib/Probability/Kernel/Composition/CompNotation.lean

Statistics

Metric	Count
Definitions «term_∘ₘ_»	1
Theorems comp_apply_univ, const_comp, deterministic_comp_eq_map, id_comp, swap_comp	5
Total	6

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_apply_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike bind ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.univ	—	bind_apply MeasurableSet.univ ProbabilityTheory.Kernel.aemeasurable MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.lintegral_const one_mul
const_comp 📖	mathematical	—	bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.const ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Set instFunLike Set.univ	—	bind_const
deterministic_comp_eq_map 📖	mathematical	Measurable	bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.deterministic map	—	bind_dirac_eq_map
id_comp 📖	mathematical	—	bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.id	—	measurable_id ProbabilityTheory.Kernel.id.eq_1 deterministic_comp_eq_map map_id
swap_comp 📖	mathematical	—	bind Prod.instMeasurableSpace DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.swap map	—	deterministic_comp_eq_map measurable_swap

ProbabilityTheory

Definitions

Name	Category	Theorems
«term_∘ₘ_» 📖	CompOp	—

---

← Back to Index