CompactFlowNeighborhood.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One compact neighborhood for all sufficiently large coordinate flows

theorem OAI.PolycyclicRecognition.exists_compact_eventual_flow_image line 16

Source documentation

Compact convergence of coordinate paths allows one compact cutoff to contain the entire late family inside the prescribed open chart.

theorem exists_compact_eventual_flow_image
    {X Y ι : Type*} [TopologicalSpace X] [MetricSpace Y] [LocallyCompactSpace Y]
    {l : Filter ι} {F : ι → X → Y} {f : X → Y} {K : Set X} {U : Set Y}
    (hK : IsCompact K) (hf : ContinuousOn f K) (hU : IsOpen U)
    (himage : f '' K ⊆ U) (hF : TendstoUniformlyOn F f l K) :
    ∃ Q : Set Y, IsCompact Q ∧ Q ⊆ U ∧ f '' K ⊆ Q ∧
      ∀ᶠ i in l, F i '' K ⊆ Q := by
…