le_mkMetric — Mathlib

English

Given m, μ, r > 0 and hr, μ ≤ mkMetric m holds if diam constraints are satisfied.

Русский

Пусть m, μ, r > 0; тогда выполняется μ ≤ mkMetric m при соблюдении ограничений диаметра.

LaTeX

$$$ μ ≤ mkMetric m $$$

Lean4

theorem le_mkMetric (m : ℝ≥0∞ → ℝ≥0∞) (μ : Measure X) (ε : ℝ≥0∞) (h₀ : 0 < ε)
    (h : ∀ s : Set X, diam s ≤ ε → μ s ≤ m (diam s)) : μ ≤ mkMetric m :=
  by
  rw [← toOuterMeasure_le, mkMetric_toOuterMeasure]
  exact OuterMeasure.le_mkMetric m μ.toOuterMeasure ε h₀ h

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