Theorems · Theorem · measure theory
MeasureTheory.OuterMeasure.mono
∀ {α : Type u_2} (self : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α}, s₁ ⊆ s₂ → self.measureOf s₁ ≤ self.measureOf s₂- Defined in
- Mathlib.MeasureTheory.OuterMeasure.Defs
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- ENNRealstatement · cited by 9,879
- MeasureTheory.OuterMeasurestatement and proof · cited by 287
- MeasureTheory.OuterMeasure.measureOfstatement · cited by 7
Cited by36
Results whose statement or proof uses this declaration.
- MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_leproof · cited by 7
- MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSupproof · cited by 7
- MeasureTheory.FiniteMeasure.apply_monoproof · cited by 5
- MeasureTheory.OuterMeasure.le_ofFunctionproof · cited by 5
- MeasureTheory.measure_symmDiff_leproof · cited by 4
- MeasureTheory.OuterMeasure.comap_iInfproof · cited by 3
- MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trimproof · cited by 3
- IsAddFoelner.tendsto_nhds_meanproof · cited by 3
- MeasureTheory.measure_lt_top_of_subsetproof · cited by 3
- IsFoelner.tendsto_nhds_meanproof · cited by 3
- Set.measure_eq_iInf_isOpenproof · cited by 3
- MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_interproof · cited by 2