OAI/Analysis/CircleDomains/Selection/JumpChainEdges.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The concrete edges in a chain with fixed old jump disks. True edges are actual allowed physical paths, and jump edges keep their original toll.

  1. def OAI.CircleDomainRigidity.physicalJumpEdge line 20
  2. theorem OAI.CircleDomainRigidity.physicalJumpEdge_of_path line 29
  3. theorem OAI.CircleDomainRigidity.physicalJumpEdge_of_jump line 37