Theorems · Theorem · measure theory
MeasureTheory.SimpleFunc.finite_range
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β), (Set.range ⇑f).Finite- Cited by
- 8 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- Set.rangestatement · cited by 4,705
- Set.Finitestatement · cited by 1,814
- MeasureTheory.SimpleFuncstatement and proof · cited by 411
- MeasureTheory.SimpleFunc.finite_range'proof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- MeasureTheory.SimpleFunc.rangeproof · cited by 97
- MeasureTheory.StronglyMeasurable.monoproof · cited by 27
- MeasureTheory.SimpleFunc.mem_rangeproof · cited by 13
- MeasureTheory.SimpleFunc.coe_rangeproof · cited by 11
- MeasureTheory.StronglyMeasurable.isSeparable_rangeproof · cited by 10
- MeasureTheory.IsStronglyPredictable.measurable_add_oneproof · cited by 6
- MeasureTheory.SimpleFunc.toLargerSpaceproof · cited by 4
- MeasureTheory.IsStronglyPredictable.of_measurable_add_oneproof · cited by 4
- MeasureTheory.IsStronglyPredictable.isStronglyProgressiveproof · cited by 3
- MeasureTheory.SimpleFunc.measurableSet_cutproof · cited by 2