Theorems · Theorem · measure theory
MeasureTheory.VectorMeasure.IntegrableOn.mono
∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s t : Set X},
MeasurableSet s → t ⊆ s → μ.IntegrableOn f s → μ.IntegrableOn f t- Cited by
- 4 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
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
- TopologicalSpaceproof · cited by 24,529
- NormedAddCommGroupstatement and proof · cited by 15,752
- MeasurableSpacestatement and proof · cited by 13,106
- AddCommMonoidproof · cited by 12,281
- MeasureTheory.Measureproof · cited by 10,939
- MeasurableSetstatement and proof · cited by 3,075
- le_rflproof · cited by 1,558
- MeasureTheory.VectorMeasurestatement and proof · cited by 451
- MeasureTheory.VectorMeasure.variationproof · cited by 125
- MeasureTheory.VectorMeasure.Integrableproof · cited by 63
- MeasureTheory.Measure.restrict_monoproof · cited by 33
Cited by4
Results whose statement or proof uses this declaration.
- MeasureTheory.VectorMeasure.Integrable.integrableOnproof · cited by 2
- MeasureTheory.VectorMeasure.hasSum_setIntegral_iUnionproof · cited by 1
- MeasureTheory.VectorMeasure.setIntegral_inter_add_sdiffproof · cited by 0
- MeasureTheory.VectorMeasure.setIntegral_sdiffproof · cited by 0