OAI/Combinatorics/Chromatic/Walls/GenericLineJoining.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.FiniteRayGeometry.wedge_ne_of_difference_ne line 12
  2. lemma OAI.ElementaryPositivity.FiniteRayGeometry.GenericOffset.join line 28
  3. lemma OAI.ElementaryPositivity.FiniteRayGeometry.GenericOffset.join_reverse line 45
  4. lemma OAI.ElementaryPositivity.FiniteRayGeometry.generic_for_two_directions line 70
  5. def OAI.ElementaryPositivity.QuantumTorus.RegularCovector line 120
  6. def OAI.ElementaryPositivity.QuantumTorus.segmentBetween line 123
  7. lemma OAI.ElementaryPositivity.QuantumTorus.segmentBetween_start line 142
  8. lemma OAI.ElementaryPositivity.QuantumTorus.segmentBetween_finish line 147
  9. def OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.single line 153
  10. def OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.trans line 157
  11. lemma OAI.ElementaryPositivity.QuantumTorus.regularCovector_exists line 171
  12. lemma OAI.ElementaryPositivity.QuantumTorus.generic_paths_via_intermediate line 179
  13. theorem OAI.ElementaryPositivity.QuantumTorus.generic_path_exists line 196