OAI/Topology/CoarseAssembly/LoopCircle.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Parametrizing a closed path by the circle

The interval endpoints are identified using Mathlib's quotient-circle construction. The resulting continuous map agrees with the path on the entire closed interval, including its identified endpoint.

  1. abbrev OAI.CoarseAssembly.WindingCircle line 19
  2. theorem OAI.CoarseAssembly.circle_parameter_surjective line 23
  3. def OAI.CoarseAssembly.loopCircle line 31
  4. theorem OAI.CoarseAssembly.loopCircle_apply_lt line 36
  5. theorem OAI.CoarseAssembly.loopCircle_apply line 41
  6. theorem OAI.CoarseAssembly.loopCircle_integerLift line 52
  7. theorem OAI.CoarseAssembly.loopCircle_postcompose line 58