Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.mkMetric_mono_smul

∀ {X : Type u_2} [inst : EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal} {c : ENNReal},
  c ≠ ⊤ →
    c ≠ 0 →
      m₁ ≤ᶠ[nhdsWithin 0 (Set.Ici 0)] c • m₂ →
        MeasureTheory.OuterMeasure.mkMetric m₁ ≤ c • MeasureTheory.OuterMeasure.mkMetric m₂

If c ∉ {0, ∞} and m₁ d ≤ c * m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 0] to state this), then mkMetric m₁ hm₁ ≤ c • mkMetric m₂ hm₂.

Defined in

Mathlib.MeasureTheory.Measure.Hausdorff

Cited by

2 results in Mathlib

Foundations

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

Assumes

EMetricSpace