English
Restrict a flow to an invariant set s, obtaining a flow on the subtype s.
Русский
Ограничение потока до инвариантного множества s образует поток на подмножество s.
LaTeX
$$$\text{restrict }(\varphi,s) : \tau \to (\text{Subtype } s) \to (\text{Subtype } s)$ with $(\restrict\varphi s)(t)x = \varphi(t)x$$$
Lean4
/-- Restriction of a flow onto an invariant set. -/
def restrict {s : Set α} (h : IsInvariant ϕ s) : Flow τ (↥s)
where
toFun t := (h t).restrict _ _ _
cont' := (ϕ.continuous continuous_fst continuous_subtype_val.snd').subtype_mk _
map_add' _ _ _ := Subtype.ext (map_add _ _ _ _)
map_zero' _ := Subtype.ext (map_zero_apply _ _)
