mkMetric'_toOuterMeasure — Mathlib

English

The coercion of OuterMeasure.mkMetric m coincides with Measure.mkMetric m, i.e., they are the same as functions on sets.

Русский

Приведение к функции OuterMeasure.mkMetric m совпадает с Measure.mkMetric m.

LaTeX

$$$ \text{The coercion } (OuterMeasure.mkMetric m) = (Measure.mkMetric m) $$$

Lean4

@[simp]
theorem mkMetric'_toOuterMeasure (m : Set X → ℝ≥0∞) : (mkMetric' m).toOuterMeasure = (OuterMeasure.mkMetric' m).trim :=
  rfl

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