Theorems · Theorem · measure theory

MeasureTheory.Measure.mkMetric_mono

∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  {m₁ m₂ : ENNReal → ENNReal}, m₁ ≤ᶠ[nhds 0] m₂ → MeasureTheory.Measure.mkMetric m₁ ≤ MeasureTheory.Measure.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 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpaceMeasurableSpaceBorelSpace