OAI/RingTheory/BassTrace/Coning.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.Cuts.vertexMean line 13
  2. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_mem_convexHull line 16
  3. lemma OAI.BassTrace.Sparse.Cuts.linear_vertexMean line 22
  4. lemma OAI.BassTrace.Sparse.Cuts.linear_vertexMean_le line 26
  5. lemma OAI.BassTrace.Sparse.Cuts.linear_vertexMean_eq_iff line 35
  6. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_eq_centroid line 53
  7. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_map line 60
  8. def OAI.BassTrace.Sparse.Cuts.cell line 68
  9. lemma OAI.BassTrace.Sparse.Cuts.exists_ray_boundary line 71
  10. lemma OAI.BassTrace.Sparse.Cuts.bounded_cell_positive_direction line 121
  11. lemma OAI.BassTrace.Sparse.Cuts.bounded_exists_ray_boundary line 144
  12. lemma OAI.BassTrace.Sparse.Cuts.boundary_ray_unique line 156
  13. lemma OAI.BassTrace.Sparse.Cuts.linear_eq_on_affineSpan line 185
  14. lemma OAI.BassTrace.Sparse.Cuts.affineIndependent_of_prefix_hyperplanes line 192
  15. lemma OAI.BassTrace.Sparse.Cuts.convexHull_inter_supporting line 220
  16. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_notMem_supporting_affineSpan line 259
  17. lemma OAI.BassTrace.Sparse.Cuts.exists_positive_ray_of_mem_convexHull_insert line 269
  18. def OAI.BassTrace.Sparse.Cuts.radialBoundary line 291
  19. lemma OAI.BassTrace.Sparse.Cuts.center_notMem_radialBoundary line 295
  20. lemma OAI.BassTrace.Sparse.Cuts.cone_hull_inter line 300
  21. lemma OAI.BassTrace.Sparse.Cuts.cone_hull_inter_boundary line 328
  22. lemma OAI.BassTrace.Sparse.Cuts.affineIndependent_insert line 351
  23. def OAI.BassTrace.Sparse.Cuts.coneFaces line 377
  24. lemma OAI.BassTrace.Sparse.Cuts.mem_coneFaces_iff line 380
  25. lemma OAI.BassTrace.Sparse.Cuts.coneFaces_down_closed line 385
  26. lemma OAI.BassTrace.Sparse.Cuts.center_mem_hull_coneFace_iff line 418
  27. lemma OAI.BassTrace.Sparse.Cuts.coneFaces_inter_subset line 433
  28. def OAI.BassTrace.Sparse.Cuts.coneComplex line 481
  29. lemma OAI.BassTrace.Sparse.Cuts.coneComplex_finite line 498
  30. lemma OAI.BassTrace.Sparse.Cuts.center_notMem_affineSpan_boundaryFace line 507
  31. lemma OAI.BassTrace.Sparse.Cuts.mem_coneComplex_space_iff line 521
  32. lemma OAI.BassTrace.Sparse.Cuts.convex_cell line 554
  33. lemma OAI.BassTrace.Sparse.Cuts.coneComplex_space_eq_cell line 564