toOuterMeasure_top

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.toOuterMeasure_top

English

The top measure equals the top outer measure via toOuterMeasure.

Русский

Верхняя мера равна верхней внешней мере через toOuterMeasure.

LaTeX

$$$ (\\top : Measure α).toOuterMeasure = (\\top : OuterMeasure α) $$$

Lean4

@[simp]
theorem toOuterMeasure_top {_ : MeasurableSpace α} : (⊤ : Measure α).toOuterMeasure = (⊤ : OuterMeasure α) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru