OAI/Analysis/CircleDomains/Selection/FiniteJumpSystems.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite jump systems and their successive extensions. The label type is retained, so adjoining a level preserves every previously installed edge.

  1. structure OAI.CircleDomainRigidity.FiniteJumpSystem line 16
  2. def OAI.CircleDomainRigidity.FiniteJumpSystem.empty line 26
  3. def OAI.CircleDomainRigidity.FiniteJumpSystem.append line 29
  4. def OAI.CircleDomainRigidity.FiniteJumpSystem.edge line 38
  5. theorem OAI.CircleDomainRigidity.FiniteJumpSystem.edge_append_old line 43
  6. theorem OAI.CircleDomainRigidity.FiniteJumpSystem.edge_append_new line 52