Theorems · Theorem · probability
ProbabilityTheory.Kernel.swap_swap
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
(ProbabilityTheory.Kernel.swap α β).comp (ProbabilityTheory.Kernel.swap β α) = ProbabilityTheory.Kernel.id- Cited by
- 4 results in Mathlib
- Foundations
- Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- ProbabilityTheory.Kernelstatement · cited by 1,281
- Measurable.compproof · cited by 234
- ProbabilityTheory.Kernel.compstatement · cited by 129
- ProbabilityTheory.Kernel.idstatement and proof · cited by 72
- ProbabilityTheory.Kernel.deterministicproof · cited by 57
- measurable_swapproof · cited by 42
- ProbabilityTheory.Kernel.swapstatement · cited by 27
- ProbabilityTheory.Kernel.deterministic_comp_deterministicproof · cited by 2
- ProbabilityTheory.Kernel.deterministic.congr_simpproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- ProbabilityTheory.swap_compProd_posteriorproof · cited by 2
- ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelCompproof · cited by 2
- ProbabilityTheory.posterior_prod_id_compproof · cited by 1
- ProbabilityTheory.posterior_posteriorproof · cited by 0