Invariant sets and basic flow lemmas #
This file supplements Mathlib's IsInvariant predicate and Flow API from
Mathlib.Dynamics.Flow.
Main declarations #
IsInvariant.apply_mem_iff: membership in a subset invariant under a family of maps with inverses is unchanged by each map.Flow.apply_comm: the maps of a flow by a commutative time monoid commute.Flow.orbit_apply: flowing a point does not change its orbit.Flow.orbit_reverse: reversing time does not change the orbits.Flow.exists_forall_exists_mem_Ioo_apply_mem: if the forward orbits of the points of a compact set all meet an open set, they all meet it before a common time.
theorem
IsInvariant.apply_mem_iff
{G : Type u_1}
{X : Type u_2}
[Inv G]
{ϕ : G → X → X}
{s : Set X}
(hs : IsInvariant ϕ s)
(hϕ : ∀ (g : G) (x : X), ϕ g⁻¹ (ϕ g x) = x)
(g : G)
(x : X)
:
Membership in a subset invariant under a family of maps with inverses is unchanged by each map.
theorem
Flow.apply_comm
{τ : Type u_1}
{α : Type u_2}
[TopologicalSpace τ]
[TopologicalSpace α]
[AddCommMonoid τ]
(ϕ : Flow τ α)
(s t : τ)
(x : α)
:
The maps of a flow by a commutative time monoid commute.
@[simp]
theorem
Flow.orbit_apply
{τ : Type u_1}
{α : Type u_2}
[TopologicalSpace τ]
[TopologicalSpace α]
[AddGroup τ]
(ϕ : Flow τ α)
(s : τ)
(x : α)
:
All points of an orbit have the same orbit.
@[simp]
theorem
Flow.orbit_reverse
{τ : Type u_1}
{α : Type u_2}
[TopologicalSpace τ]
[TopologicalSpace α]
[SubtractionCommMonoid τ]
[ContinuousNeg τ]
(ϕ : Flow τ α)
(x : α)
:
Reversing time does not change the orbits of a flow.
theorem
Flow.exists_forall_exists_mem_Ioo_apply_mem
{τ : Type u_1}
{α : Type u_2}
[TopologicalSpace τ]
[TopologicalSpace α]
[AddMonoid τ]
[LinearOrder τ]
[NoMaxOrder τ]
(ϕ : Flow τ α)
{C W : Set α}
(hC : IsCompact C)
(hW : IsOpen W)
(h : ∀ x ∈ C, ∃ t > 0, ϕ.toFun t x ∈ W)
:
A uniform time to reach an open set. If the forward orbit of every point of a compact set
C meets an open set W at some positive time, then there is one time T such that each of these
orbits meets W at some time in (0, T).