Theorems · Theorem · measure theory
MeasurableSpace.comap_iSup
∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {g : β → α} {m : ι → MeasurableSpace α},
MeasurableSpace.comap g (⨆ i, m i) = ⨆ i, MeasurableSpace.comap g (m i)- Cited by
- 4 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- iSupstatement · cited by 2,415
- MeasurableSpace.comapstatement · cited by 124
- GaloisConnection.l_iSupproof · cited by 78
- MeasurableSpace.gc_comap_mapproof · cited by 10
Cited by4
Results whose statement or proof uses this declaration.
- measurable_pi_iffproof · cited by 21
- MeasureTheory.measurable_cylinderEvents_iffproof · cited by 2
- MeasurableSpace.comap_process_piproof · cited by 1
- MeasurableSpace.comap_le_comap_piproof · cited by 0