English
Let s be a subset invariant under ϕ. Then the orbit of x (lying in s) under the restricted flow ϕ|s is exactly the preimage of the original orbit under the inclusion map Subtype.val.
Русский
Пусть s — подмножество, инвариантное относительно ϕ. Орбита точки x в ограниченном потоке ϕ|s равна пересечению орбиты ϕ x с s, то есть равна образу подмножества s через включение.
LaTeX
$$$orbit(\\\\varphi\\\\|_s)\\\\ x = \\\\operatorname{Subtype.val}^{-1}'(orbit(\\\\varphi) x).$$$
Lean4
theorem orbit_restrict (s : Set α) (hs : IsInvariant ϕ s) (x : s) :
orbit (ϕ.restrict hs) x = Subtype.val ⁻¹' orbit ϕ x :=
Set.ext (fun x => by simp [orbit_eq_range, Subtype.ext_iff])
