Theorems · Theorem · measure theory
Measurable.indicator
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
[inst : Zero β], Measurable f → MeasurableSet s → Measurable (s.indicator f)- Cited by
- 38 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Zero
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.
- Setstatement and proof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasurableSetstatement and proof · cited by 3,075
- Measurablestatement and proof · cited by 1,499
- Set.indicatorstatement · cited by 723
- measurable_constproof · cited by 156
- Measurable.piecewiseproof · cited by 9
Cited by38
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.compProd_applyproof · cited by 31
- MeasureTheory.setLIntegral_condLExpproof · cited by 8
- measurable_indicator_const_iffproof · cited by 4
- MeasureTheory.Measure.mconv_absolutelyContinuousproof · cited by 3
- MeasureTheory.Measure.measurable_diracproof · cited by 3
- MeasureTheory.measure_add_lintegral_eqproof · cited by 3
- MeasureTheory.measure_mul_lintegral_eqproof · cited by 3
- MeasureTheory.StronglyAdapted.measurable_upcrossingsBeforeproof · cited by 3
- MeasureTheory.lintegral_indicator_const_compproof · cited by 3
- MeasureTheory.Measure.conv_absolutelyContinuousproof · cited by 3
- aemeasurable_indicator_iffproof · cited by 2
- ProbabilityTheory.IdentDistrib.truncationproof · cited by 2