OAI/Topology/CoarseAssembly/CompactFamilyHomotopy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Norm continuity of pullback along component-preserving family homotopies

  1. def OAI.CoarseAssembly.Analytic.compactFamilySlice line 20
  2. theorem OAI.CoarseAssembly.Analytic.compactFamilyPullback_continuous line 24
  3. def OAI.CoarseAssembly.Analytic.compactFamilyCycleHomotopy line 63
  4. theorem OAI.CoarseAssembly.Analytic.compactFamily_homotopy_invariance line 77

    Source documentation

    Componentwise compact homotopies give a proper family homotopy on analytic classes.

    theorem compactFamily_homotopy_invariance (f g : ∀ j, C(X j, Y j))
    (H : ∀ j, (f j).Homotopy (g j)) :
    pushforward (compactFamilyMap f) = pushforward (compactFamilyMap g) := by
…

    Mentions: OAI.CoarseAssembly.Analytic.pushforward, OAI.CoarseAssembly.compactFamilyMap