iSup_coe_eapprox

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.iSup_coe_eapprox

English

For measurable f, the iSup of the functions (eapprox f n) equals f as a function.

Русский

Для измеримой f верхняя супремума функций eapprox f n равна f как функция.

LaTeX

$$$ \bigsqcup_{n} \big( eapprox f n \big) = f $$$

Lean4

theorem iSup_coe_eapprox (hf : Measurable f) : ⨆ n, ⇑(eapprox f n) = f := by
  simpa [funext_iff] using iSup_eapprox_apply hf

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

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

Разделы

Аффилиация

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