Theorems · Theorem · dynamical systems

Flow.omegaLimit_omegaLimit

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

Defined in

Mathlib.Dynamics.OmegaLimit

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommGroupTopologicalSpace