Theorems · Theorem · measure theory
MeasurableSpace.comap_generateFrom
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)},
MeasurableSpace.comap f (MeasurableSpace.generateFrom s) = MeasurableSpace.generateFrom (Set.preimage f '' s)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- MeasurableSpacestatement · cited by 13,106
- Set.imagestatement and proof · cited by 5,609
- Set.preimagestatement and proof · cited by 4,946
- MeasurableSetproof · cited by 3,075
- le_antisymmproof · cited by 2,068
- Set.mem_image_of_memproof · cited by 371
- MeasurableSpace.generateFromstatement · cited by 172
- MeasurableSpace.comapstatement · cited by 124
- MeasurableSpace.generateFrom_leproof · cited by 49
- MeasurableSpace.comap_le_iff_le_mapproof · cited by 10
Cited by7
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetproof · cited by 8
- ProbabilityTheory.Kernel.IndepFun.process_indepFunproof · cited by 4
- ProbabilityTheory.Kernel.iIndepFun.iIndepFun_processproof · cited by 2
- generateFrom_pi_eqproof · cited by 1
- generateFrom_prod_eqproof · cited by 1
- borel_comapproof · cited by 1
- MeasurableSpace.CountablyGenerated.comapproof · cited by 0