OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryFamilyHomeomorphism.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.boundary_family_homeomorphisms_of_compact_shadows line 17

   Source documentation

   Contracting rays turn the two compact shadows of a coarse inverse pair into inverse boundary maps. This applies to all members of a family with the same compact shadow sets.

   theorem boundary_family_homeomorphisms_of_compact_shadows
       {P G S T : Type*} [Group G] [MetricSpace G] [IsTopologicalGroup G]
       [IsIsometricSMul G G] [ProperSpace G]
       [One S] [TopologicalSpace S] [T2Space S]
       [One T] [TopologicalSpace T] [T2Space T]
       (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T)
       (hcontS : ∀ g, Continuous (actS g)) (hcontT : ∀ g, Continuous (actT g))
       (σS : S → G) (hσS : Continuous σS) (hsectionS : ∀ q, actS (σS q) 1 = q)
       (σT : T → G) (hσT : Continuous σT) (hsectionT : ∀ q, actT (σT q) 1 = q)
       (rayS rayT : ℕ → G)
       (hfixS : ∀ n, actS (rayS n) 1 = 1) (hfixT : ∀ n, actT (rayT n) 1 = 1)
       (hcontractS : ∀ K : Set G, IsCompact K → ∀ k : ℕ → G,
   …