mkMetric_nnreal_smul — Mathlib

English

Let m be a function ℝ≥0∞ → ℝ≥0∞ and c ∈ ℝ≥0 with c ≠ 0. Then the outer metric measure satisfies (mkMetric (c • m) : OuterMeasure X) = c • mkMetric m.

Русский

Пусть m: ℝ≥0∞ → ℝ≥0∞ и c ∈ ℝ≥0 с c ≠ 0. Тогда внешняя мера, порождаемая mkMetric, удовлетворяет (mkMetric (c • m) : OuterMeasure X) = c • mkMetric m.

LaTeX

$$$ (mkMetric (c \cdot m) : OuterMeasure X) = c \cdot mkMetric m $$$

Lean4

theorem mkMetric_nnreal_smul (m : ℝ≥0∞ → ℝ≥0∞) {c : ℝ≥0} (hc : c ≠ 0) :
    (mkMetric (c • m) : OuterMeasure X) = c • mkMetric m := by
  rw [ENNReal.smul_def, ENNReal.smul_def, mkMetric_smul m ENNReal.coe_ne_top (ENNReal.coe_ne_zero.mpr hc)]

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