OAI/Geometry/RCD/Sobolev/ConvexDifferenceSpace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The vector space generated by differences of a convex set

  1. def OAI.RegularPointCoordinates.convexDifferenceSpace line 15

    Source documentation

    Every vector is one nonnegative multiple of a difference of two points. This representation retains the points needed for the distance pairing.

    def convexDifferenceSpace (K : Set E) (hK : Convex ℝ K) (h0 : 0 ∈ K) : Submodule ℝ E where
…
  2. theorem OAI.RegularPointCoordinates.mem_convexDifferenceSpace line 42