Theorems · Inductive type · measure theory
MeasureTheory.SimpleFunc
(α : Type u) → [MeasurableSpace α] → Type v → Type (max u v)
A function f from a measurable space to any type is called simple,
if every preimage f ⁻¹' {x} is measurable, and the range is finite. This structure bundles
a function with these properties.
- Cited by
- 411 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
Cited by454
Results whose statement or proof uses this declaration.
- MeasureTheory.StronglyMeasurableproof · cited by 363
- MeasureTheory.Lp.simpleFuncproof · cited by 122
- MeasureTheory.SimpleFunc.rangestatement and proof · cited by 97
- MeasureTheory.SimpleFunc.lintegralstatement and proof · cited by 55
- MeasureTheory.SimpleFunc.mapstatement and proof · cited by 54
- MeasureTheory.SimpleFunc.conststatement · cited by 50
- MeasureTheory.lintegral_indicatorproof · cited by 47
- MeasureTheory.Lp.simpleFunc.toSimpleFuncstatement · cited by 46
- MeasureTheory.SimpleFunc.setToSimpleFuncstatement and proof · cited by 40
- MeasureTheory.StronglyMeasurable.approxstatement · cited by 40
- MeasureTheory.SimpleFunc.approxOnstatement · cited by 39
- MeasureTheory.lintegral_mono_aeproof · cited by 36
Showing the 200 most cited of 454.