English
For a family of types g(i) with a DistribMulAction from f(i) to g(i), the dependent function space ∀ i, g(i) carries a DistribMulAction from ∀ i, f(i) with coordinatewise action: (a(i)) • x(i) for each i.
Русский
Для семейства типов g(i), на которые действует f(i) распределительно, существует распределимое действие на зависимом пространстве функций ∀ i, g(i) определяемое координатно: (a(i)) • x(i).
LaTeX
$$$\forall i, (f(i) \text{ действует на } g(i)\text{ распределительно}) \Rightarrow (\forall i, g(i)) \text{ имеетDistribMulAction от } (\forall i, f(i)),$ указанное координатно: $((a) \cdot x)(i) = a(i) \cdot x(i).$$$
Lean4
instance distribMulAction' {g : I → Type*} {m : ∀ i, Monoid (f i)} {n : ∀ i, AddMonoid <| g i}
[∀ i, DistribMulAction (f i) (g i)] :
@DistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m) (@Pi.addMonoid I g n) :=
{ Pi.mulAction', Pi.distribSMul' with }
