OAI/Combinatorics/TriangleRemoval/Process/WitnessDimensions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpTerminalLeave.WitnessDimensions line 23
  2. def OAI.SharpTerminalLeave.dimensionBirth line 26
  3. abbrev OAI.SharpTerminalLeave.BoundedEmbeddedWitness line 29
  4. instance OAI.SharpTerminalLeave.(instance at line 35) line 35
  5. def OAI.SharpTerminalLeave.embeddedWitnessPaths line 41
  6. theorem OAI.SharpTerminalLeave.traced_repeat_canonical_cover line 50