English
Flow τ α can be endowed with an additive action by τ on α via Flow.toFun, with the action maps given by map_add' and map_zero'.
Русский
Поток τ α может быть наделён аддитивным действием τ на α через Flow.toFun, операции действия заданы map_add' и map_zero'.
LaTeX
$$$\text{toAddAction}(\varphi) : \mathrm{AddAction}(\tau, \alpha)$ with $\text{vadd}=\varphi$, $\text{add\_vadd}=\varphi.map\_add'$, $\text{zero\_vadd}=\varphi.map\_zero'$$$
Lean4
/-- Restrict a flow by `τ` to a flow by an additive submonoid of `τ`. -/
def restrictAddSubmonoid (S : AddSubmonoid τ) : Flow S α
where
toFun t x := ϕ t x
cont' := ϕ.continuous (continuous_subtype_val.comp continuous_fst) continuous_snd
map_add' t₁ t₂ x := ϕ.map_add' t₁ t₂ x
map_zero' := ϕ.map_zero'
