mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Port convexity to affine spaces

Open urkud opened this issue 5 years ago • 0 comments

  • [ ] port convexity to vector spaces ([module 𝕜 E])
    • [x] redefine segment and open_segment
    • [x] redefine convex
    • [x] redefine convex_on and concave_on
    • [ ] redefine finset.center_mass
    • [x] redefine convex_hull
    • [x] redefine std_simplex
    • [ ] port the rest of the library
  • [ ] port convexity to affine spaces ([module k V] [affine_space V E])
    • [ ] redefine segment and open_segment
    • [ ] redefine convex
    • [ ] redefine convex_on and concave_on
    • [ ] redefine finset.center_mass
    • [ ] redefine convex_hull
    • [ ] redefine std_simplex
    • [ ] port the rest of the library

urkud avatar Jun 01 '20 18:06 urkud