mkMetric_smul — Mathlib

English

Scaling a metric outer measure by a positive scalar c is equivalent to scaling the corresponding outer measure mkMetric m by c.

Русский

Умножение метрической внешней меры на положительный скаляр c эквивалентно умножению соответствующей меры mkMetric m на c.

LaTeX

$$mkMetric (c • m) = c • mkMetric m$$

Lean4

theorem mkMetric_smul (m : ℝ≥0∞ → ℝ≥0∞) {c : ℝ≥0∞} (hc : c ≠ ∞) (hc' : c ≠ 0) :
    (mkMetric (c • m) : OuterMeasure X) = c • mkMetric m :=
  by
  simp only [mkMetric, mkMetric', mkMetric'.pre]
  simp_rw [smul_iSup, smul_boundedBy hc, smul_extend _ hc', Pi.smul_apply]

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