coe_completion

Mathlib.MeasureTheory.Measure.NullMeasurable

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

English

The completion map does not change the measure on sets: for all s, (μ.completion)(s) = μ(s).

Русский

Дополнение не изменяет меру на множествах: для всех s, (μ.completion)(s) = μ(s).

LaTeX

$$$\forall s:\text{Set},\ (\mu^{\mathrm{completion}})(s)=\mu(s).$$$

Lean4

@[simp]
theorem coe_completion {_ : MeasurableSpace α} (μ : Measure α) : ⇑μ.completion = μ :=
  rfl

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

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

Разделы

Аффилиация

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