Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.mkMetric_mono

∀ {X : Type u_2} [inst : EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal},
  m₁ ≤ᶠ[nhds 0] m₂ → MeasureTheory.OuterMeasure.mkMetric m₁ ≤ MeasureTheory.OuterMeasure.mkMetric m₂

If m₁ d ≤ m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝 0] to state this), then mkMetric m₁ hm₁ ≤ mkMetric m₂ hm₂.

Defined in

Mathlib.MeasureTheory.Measure.Hausdorff

Cited by

0 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpace