coeFn_toAEEqFun

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#ContinuousMap.coeFn_toAEEqFun

English

For any ContinuousMap f, the a.e. representative of f.toAEEqFun μ is just f itself, i.e., f.toAEEqFun μ =ᵐ[μ] f.

Русский

Для любой непрерывной карты f исчезает равенство по почти всей мере между f.toAEEqFun μ и самой f.

LaTeX

$$$f.toAEEqFun(\mu) =_{a.e., μ} f$$$

Lean4

theorem coeFn_toAEEqFun (f : C(α, β)) : f.toAEEqFun μ =ᵐ[μ] f :=
  AEEqFun.coeFn_mk f _

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

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

Разделы

Аффилиация

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