OAI/Topology/CoarseAssembly/CompactFamilyMap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Proper maps preserving compact components

The properness argument for the family of boundary loops uses compactness of each source component and preservation of the discrete component index.

  1. def OAI.CoarseAssembly.compactFamilyContinuousMap line 21
  2. theorem OAI.CoarseAssembly.compactFamily_preimage_compact line 25
  3. def OAI.CoarseAssembly.compactFamilyMap line 38
  4. theorem OAI.CoarseAssembly.compactFamilyMap_apply line 43