instStarOfContinuousStar — Mathlib

English

For star-valued maps with measurable structure, the star-applied function equals the function-star almost everywhere.

Русский

Для отображений со звезде и меровой структурой звезда-оператор применён к функции совпадает с функцией-звездой почти всюду.

LaTeX

$$$\\uparrow(\\mathrm{star}\\, f) =_{\\mu} (\\mathrm{star}\\, f : \\alpha \\to R)$$$

Lean4

instance [Star R] [ContinuousStar R] : Star (α →ₘ[μ] R) where star f := (AEEqFun.comp _ continuous_star f)

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