Theorems · Theorem · measure theory
MeasureTheory.VectorMeasure.neg_le_neg_iff
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommGroup M]
[inst_2 : PartialOrder M] [IsOrderedAddMonoid M] [inst_4 : IsTopologicalAddGroup M]
(v w : MeasureTheory.VectorMeasure α M) {i : Set α},
MeasurableSet i → ((-w).restrict i ≤ (-v).restrict i ↔ v.restrict i ≤ w.restrict i)- Cited by
- 3 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- AddCommGroupstatement and proof · cited by 12,871
- PartialOrderstatement and proof · cited by 6,410
- MeasurableSetstatement and proof · cited by 3,075
- IsOrderedAddMonoidstatement and proof · cited by 1,659
- IsTopologicalAddGroupstatement and proof · cited by 1,394
- neg_negproof · cited by 960
- MeasureTheory.VectorMeasurestatement and proof · cited by 451
- MeasureTheory.VectorMeasure.restrictstatement and proof · cited by 139
- MeasureTheory.VectorMeasure.neg_le_negproof · cited by 6
Cited by3
Results whose statement or proof uses this declaration.
- MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_negativeproof · cited by 0
- MeasureTheory.SignedMeasure.subset_negative_null_setproof · cited by 0