Metamath Proof Explorer


Table of Contents - 20.16.8.3. Barycentric coordinates

Lemmas about barycentric coordinates. For the moment, this is limited to the one-dimensional case (complex line), where existence and uniqueness of barycentric coordinates are proved by bj-bary1 (which computes them). It would be nice to prove the two-dimensional case (is it easier to use ad hoc computations, or Cramer formulas?), in order to do some planar geometry.

  1. bj-bary1lem
  2. bj-bary1lem1
  3. bj-bary1