OAI/RingTheory/BassTrace/FacetGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Two-sided facet incidence inside a single affine carrier, without a manifold hypothesis.

  1. lemma OAI.BassTrace.Sparse.exists_weights_of_mem_affineSpan line 19
  2. lemma OAI.BassTrace.Sparse.exists_small_positive_weights line 34
  3. lemma OAI.BassTrace.Sparse.sum_weights_mem_convexHull line 48
  4. lemma OAI.BassTrace.Sparse.same_side_cone_overlap line 62
  5. lemma OAI.BassTrace.Sparse.apex_notMem_affineSpan line 138
  6. lemma OAI.BassTrace.Sparse.exists_facet_form line 157
  7. lemma OAI.BassTrace.Sparse.affineForm_eq_on_convexHull line 179
  8. lemma OAI.BassTrace.Sparse.eq_of_facet_same_side line 184
  9. lemma OAI.BassTrace.Sparse.facet_apex_card_le_two line 201
  10. lemma OAI.BassTrace.Sparse.affineSpan_eq_of_card_eq line 245
  11. lemma OAI.BassTrace.Sparse.facet_coface_card_le_two line 255
  12. lemma OAI.BassTrace.Sparse.positiveCombination_carrier line 304
  13. lemma OAI.BassTrace.Sparse.simplex_contains_positivePoint line 328
  14. lemma OAI.BassTrace.Sparse.eventually_coface_at_positivePoint line 339
  15. theorem OAI.BassTrace.Sparse.exists_facet_coface_on_side line 361
  16. lemma OAI.BassTrace.Sparse.convexHull_inter_supporting line 422
  17. lemma OAI.BassTrace.Sparse.full_face_affineSpan line 469
  18. def OAI.BassTrace.Sparse.facetApexes line 475
  19. lemma OAI.BassTrace.Sparse.mem_facetApexes line 479
  20. lemma OAI.BassTrace.Sparse.parent_card_bound line 484
  21. lemma OAI.BassTrace.Sparse.facet_positive_apex_card line 491