Theorems · Theorem · measure theory
MeasurableEmbedding.comap_eq
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
MeasurableEmbedding f → MeasurableSpace.comap f inst_1 = inst- Cited by
- 4 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.imageproof · cited by 5,609
- MeasurableSetproof · cited by 3,075
- LE.le.antisymmproof · cited by 507
- MeasurableEmbeddingstatement and proof · cited by 170
- MeasurableSpace.comapstatement · cited by 124
- MeasurableEmbedding.injectiveproof · cited by 35
- Function.Injective.preimage_imageproof · cited by 30
- Measurable.comap_leproof · cited by 29
- MeasurableEmbedding.measurableproof · cited by 29
- MeasurableEmbedding.measurableSet_image'proof · cited by 15
Cited by4
Results whose statement or proof uses this declaration.
- MeasurableEmbedding.prodMapproof · cited by 4
- MeasurableSpace.comap_complproof · cited by 1
- MeasurableEmbedding.borelSpaceproof · cited by 1
- MeasurableEmbedding.iff_comap_eqproof · cited by 1