OAI/Topology/CoarseAssembly/ExplicitFamilyFilling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Filling the explicit circle family without countable-additivity inputs

  1. theorem OAI.CoarseAssembly.windingCircleCycle_representation_const line 16
  2. theorem OAI.CoarseAssembly.circleFamily_constant_degenerate line 27
  3. theorem OAI.CoarseAssembly.explicitCircleFamily_constant_zero line 62
  4. theorem OAI.CoarseAssembly.explicitCircleFamily_filled_zero line 69
  5. theorem OAI.CoarseAssembly.explicitBaseBoundaryFamily_zero line 80