OAI/Analysis/SphereIsometry/BarycentricBasic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite barycenters

The point attached to a nonempty face in barycentric subdivision is its ordinary finite average. The definition also assigns zero to the empty set.

  1. def OAI.Tingley.finiteBarycenter line 23
  2. theorem OAI.Tingley.finiteBarycenter_eq_centerMass line 26
  3. theorem OAI.Tingley.finiteBarycenter_empty line 30
  4. theorem OAI.Tingley.finiteBarycenter_singleton line 34
  5. theorem OAI.Tingley.finiteBarycenter_congr line 38
  6. theorem OAI.Tingley.finiteBarycenter_mem_convex line 45
  7. theorem OAI.Tingley.finiteBarycenter_mem_convexHull line 55
  8. theorem OAI.Tingley.map_finiteBarycenter line 62
  9. theorem OAI.Tingley.finiteBarycenter_map line 66
  10. theorem OAI.Tingley.finiteBarycenter_map_of_eq line 70
  11. theorem OAI.Tingley.finiteBarycenter_apply line 76