English
If the star operation on the codomain R is trivial (r* = r for all r) and the star is continuous, then the star on the space of μ-almost everywhere equivalence classes of μ-measurable maps α → R is the trivial star. In particular, every class is fixed by the star: f* = f.
Русский
Если операция звезды на многозначном кольце R тривиальна (для всех r применима r* = r) и звезда непрерывна, тогда звезда на пространство эквивалентностей функций с точки зрения μ (μ-почти всюду измеримы) из α в R также тривиальна: для любого класса f выполняется f* = f.
LaTeX
$$$\forall f \in \mathrm{AEEqFun}(\alpha, R, \mu),\ f^{\*} = f.$$$
Lean4
instance [Star R] [TrivialStar R] [ContinuousStar R] : TrivialStar (α →ₘ[μ] R) where
star_trivial f := show comp _ _ f = f by simp [funext star_trivial, ← Function.id_def]
