mkMetric_mono_smul — Mathlib

English

If c ≠ ∞ and c ≠ 0 and m1 ≤ᶠ[𝓝[≥] 0] c • m2, then (mkMetric m1) ≤ c • (mkMetric m2).

Русский

Если c ≠ ∞ и c ≠ 0 и m1 сопоставимо с c • m2 с помощью предика, то mkMetric m1 ≤ c • mkMetric m2.

LaTeX

$$$ (mkMetric m1) \le c \cdot (mkMetric m2) $$$

Lean4

/-- 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₂`. -/
theorem mkMetric_mono_smul {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} {c : ℝ≥0∞} (hc : c ≠ ∞) (h0 : c ≠ 0) (hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂) :
    (mkMetric m₁ : Measure X) ≤ c • mkMetric m₂ := fun s ↦
  by
  rw [← OuterMeasure.coe_mkMetric, coe_smul, ← OuterMeasure.coe_mkMetric]
  exact OuterMeasure.mkMetric_mono_smul hc h0 hle s

Похожие утверждения