measureOf_eq_coe — Mathlib

English

For any outer measure m on α, the function measureOf coincides with m; i.e., the two ways of viewing the measure agree on every set.

Русский

Для любой внешней меры m на α функция measureOf совпадает с самой мерой; то есть два способа задания меры совпадают на любом множестве.

LaTeX

$$$m.\\mathrm{measureOf} = m$$$

Lean4

@[simp]
theorem measureOf_eq_coe (m : OuterMeasure α) : m.measureOf = m :=
  rfl

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