Restriction of ambient isotopies

An ambient isotopy preserving a subset at every time restricts to an ambient isotopy of that subset, with its subspace topology. No openness or closedness is required: the inverse total map restricts as well. This allows an isotopy supported in a closed ball to be read as an isotopy of the ball itself.

def TauCeti.AmbientIsotopy.restrict {X : Type u_1} [TopologicalSpace X] (Φ : AmbientIsotopy X) (s : Set X) (hs : ∀ (t : ↑unitInterval) (x : X), Φ.toContinuousMap (t, x) ∈ s ↔ x ∈ s) : AmbientIsotopy ↑s

Restrict an ambient isotopy to a subset preserved by each time slice in both directions.

@[simp]

theorem TauCeti.AmbientIsotopy.coe_restrict_apply {X : Type u_1} [TopologicalSpace X] (Φ : AmbientIsotopy X) (s : Set X) (hs : ∀ (t : ↑unitInterval) (x : X), Φ.toContinuousMap (t, x) ∈ s ↔ x ∈ s) (p : ↑unitInterval × ↑s) : ↑((Φ.restrict s hs).toContinuousMap p) = Φ.toContinuousMap (p.1, ↑p.2)

Restriction leaves the underlying pointwise motion unchanged.