OAI/Combinatorics/Chromatic/Walls/CompletedPathAction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RationalFiber.comparisonWordAction_append line 11
  2. lemma OAI.ElementaryPositivity.RationalFiber.comparisonWordAction_input_congr line 20
  3. lemma OAI.ElementaryPositivity.RationalFiber.actualPathWord_trans line 45
  4. def OAI.ElementaryPositivity.RationalFiber.actualPathAction line 55
  5. lemma OAI.ElementaryPositivity.RationalFiber.actualPathAction_coeff line 64
  6. theorem OAI.ElementaryPositivity.RationalFiber.actualPathAction_loop line 78
  7. theorem OAI.ElementaryPositivity.RationalFiber.actualPathAction_trans line 87
  8. def OAI.ElementaryPositivity.QuantumTorus.GenericLineSegment.avoidsCut line 115
  9. def OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.avoidsCut line 118
  10. def OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.castEnds line 123
  11. lemma OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.avoidsCut_castEnds line 126
  12. lemma OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.avoidsCut_trans line 131
  13. lemma OAI.ElementaryPositivity.QuantumTorus.segment_avoidsCut_of_sign line 139
  14. theorem OAI.ElementaryPositivity.QuantumTorus.generic_path_avoiding_cut_exists line 163