Theorems · Theorem · dynamical systems

Flow.isInvariant_omegaLimit

∀ {τ : Type u_1} [inst : TopologicalSpace τ] [inst_1 : AddMonoid τ] {α : Type u_2} [inst_2 : TopologicalSpace α]
  (f : Filter τ) (ϕ : Flow τ α) (s : Set α),
  (∀ (t : τ), Filter.Tendsto (fun x => t + x) f f) → IsInvariant ϕ.toFun (omegaLimit f ϕ.toFun s)

Defined in

Mathlib.Dynamics.OmegaLimit

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddMonoidTopologicalSpace