Theorems · Theorem · measure theory
MeasureTheory.SimpleFunc.measurableSet_fiber
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (x : β),
MeasurableSet (⇑f ⁻¹' {x})- Cited by
- 20 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- Set.preimagestatement · cited by 4,946
- MeasurableSetstatement · cited by 3,075
- MeasureTheory.SimpleFuncstatement and proof · cited by 411
- MeasureTheory.SimpleFunc.measurableSet_fiber'proof · cited by 2
Cited by20
Results whose statement or proof uses this declaration.
- MeasureTheory.SimpleFunc.setToSimpleFunc_congrproof · cited by 10
- MeasureTheory.SimpleFunc.map_setToSimpleFuncproof · cited by 6
- MeasureTheory.IsStronglyPredictable.measurable_add_oneproof · cited by 6
- MeasureTheory.IsStronglyPredictable.of_measurable_add_oneproof · cited by 4
- MeasureTheory.IsStronglyPredictable.isStronglyProgressiveproof · cited by 3
- MeasureTheory.SimpleFunc.sum_measure_preimage_singletonproof · cited by 2
- MeasureTheory.SimpleFunc.measurableSet_supportproof · cited by 2
- MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left'proof · cited by 2
- MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'proof · cited by 2
- MeasureTheory.SimpleFunc.simpleFunc_botproof · cited by 2
- MeasureTheory.SimpleFunc.measurableSet_cutproof · cited by 2