OAI/Topology/CoarseAssembly/FiberConnected.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Connectivity of the finite fibered graphs

Transport from a singleton boundary fiber reaches every vertex: its image is the normalized constant vector, which has no zero coordinate. Thus connectivity does not require an additional Cayley-generation assumption.

  1. theorem OAI.CoarseAssembly.discBoundaryBase_depth line 20
  2. theorem OAI.CoarseAssembly.constant_coordinate_ne_zero line 24
  3. theorem OAI.CoarseAssembly.fiberBoundary_reaches line 31
  4. theorem OAI.CoarseAssembly.fiberedGraph_connected line 53