Theorems · Theorem · dynamical systems

eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset

∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [T2Space β] {c : Set β},
  IsCompact c →
    (∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) →
      ∀ {n : Set β}, IsOpen n → omegaLimit f ϕ s ⊆ n → ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n

A set is eventually carried into any open neighbourhood of its ω-limit: if c is a compact set such that closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c for some v ∈ f and n is an open neighbourhood of ω f ϕ s, then for some u ∈ f we have closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n.

Defined in

Mathlib.Dynamics.OmegaLimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2Space