OAI/Combinatorics/Chromatic/Walls/FiniteRayGeometry.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.FiniteRayGeometry.dual_avoid_in_annihilator line 12
  2. lemma OAI.ElementaryPositivity.FiniteRayGeometry.scalar_sign_epsilon line 27
  3. lemma OAI.ElementaryPositivity.FiniteRayGeometry.preserve_finite_signs line 43
  4. lemma OAI.ElementaryPositivity.FiniteRayGeometry.generic_offset line 59
  5. def OAI.ElementaryPositivity.FiniteRayGeometry.forbidden line 80
  6. structure OAI.ElementaryPositivity.FiniteRayGeometry.GenericOffset line 85
  7. lemma OAI.ElementaryPositivity.FiniteRayGeometry.exists_generic_offset line 91
  8. lemma OAI.ElementaryPositivity.FiniteRayGeometry.GenericOffset.parallel_avoided line 104
  9. lemma OAI.ElementaryPositivity.FiniteRayGeometry.GenericOffset.joint_plane line 110
  10. lemma OAI.ElementaryPositivity.QuantumTorus.positive_ray_of_mem_span line 144
  11. def OAI.ElementaryPositivity.QuantumTorus.lineEvents line 156
  12. lemma OAI.ElementaryPositivity.QuantumTorus.mem_lineEvents_iff line 159
  13. def OAI.ElementaryPositivity.QuantumTorus.realRootsThrough line 177
  14. lemma OAI.ElementaryPositivity.QuantumTorus.realRoot_mem line 181
  15. lemma OAI.ElementaryPositivity.QuantumTorus.line_generic line 186
  16. lemma OAI.ElementaryPositivity.QuantumTorus.real_line_signs line 202
  17. lemma OAI.ElementaryPositivity.QuantumTorus.line_cell_signs line 224