toGerm_eq

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.toGerm_eq

English

The toGerm of mk f hf equals the underlying coeFn representation under Germ.ofFun cast.

Русский

toGerm mk f hf равен базовому представлению fn через Germ.ofFun.

LaTeX

$$$toGerm\_eq: (mk f hf).toGerm = (f : α \to β) \text{ cast to germ}$$$

Lean4

theorem toGerm_eq (f : α →ₘ[μ] β) : f.toGerm = (f : α → β) := by rw [← mk_toGerm f f.aestronglyMeasurable, mk_coeFn]

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

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

Разделы

Аффилиация

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