English
Induction principle for simple functions: to prove P(f) for all simple functions f, it suffices to prove P for constant functions and that P is closed under piecewise combination on measurable sets.
Русский
Индукционное свойство для простых функций: чтобы доказать P(f) для любой простой функции, достаточно доказать P(константы) и то, что P сохраняется при разбиении по множествам измеримых.
LaTeX
$$$\\text{induction'}\\; {P}:\\; (\\forall c, P(\\text{const }\\alpha c)) \\,\\land \\, (\\forall f,g,\\;\\forall s,\\; \\text{MeasurableSet } s \\Rightarrow P(f) \\Rightarrow P(g) \\Rightarrow P(f\\,\\text{piecewise } s\\, \\text{hs } g)) \\Rightarrow \\forall f, P(f).$$$
Lean4
@[to_additive existing]
instance instMonoid [Monoid β] : Monoid (α →ₛ β) :=
fast_instance%Function.Injective.monoid (fun f => show α → β from f) coe_injective coe_one coe_mul coe_pow
