OAI/GroupTheory/PolycyclicRecognition/Analysis/ProfileCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_compact_containing_profiles line 18

   Source documentation

   Equicontinuous profiles with pointwise bounded values lie in one compact set for locally uniform convergence. The domain need not itself be compact.

   theorem exists_compact_containing_profiles
       (F : I → C(X, W)) (hequi : Equicontinuous (fun i x => F i x))
       (w₀ : W) (hbound : ∀ x, ∃ R : ℝ, ∀ i, dist (F i x) w₀ ≤ R) :
       ∃ S : Set C(X, W), IsCompact S ∧ ∀ i, F i ∈ S := by
   …