Theorems · Definition · measure theory
MeasurableSpace.comap
{α : Type u_1} → {β : Type u_2} → (α → β) → MeasurableSpace β → MeasurableSpace αThe reverse image of a measurable space under a function. comap f m contains the sets
s : Set α such that s is the f-preimage of a measurable set in β.
- Cited by
- 124 results in Mathlib
- Foundations
- Depth 12 from the axioms, rests on 47 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- Set.preimageproof · cited by 4,946
- MeasurableSetproof · cited by 3,075
Cited by131
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.IndepFunproof · cited by 70
- ProbabilityTheory.Kernel.iIndepFunproof · cited by 65
- Measurable.comap_lestatement · cited by 29
- measurable_pi_iffproof · cited by 21
- MeasurableSpace.prodproof · cited by 15
- Measurable.of_comap_lestatement · cited by 10
- MeasureTheory.cylinderEventsproof · cited by 10
- MeasurableSpace.comap_compstatement · cited by 10
- MeasurableSpace.comap_le_iff_le_mapstatement and proof · cited by 10
- MeasurableSpace.gc_comap_mapstatement · cited by 10
- comap_measurablestatement · cited by 9
- measurable_iff_comap_lestatement · cited by 8