Affine space #
In this file we introduce the following notation:
AffineSpace V Pis an alternative notation for
AddTorsor V Pintroduced at the end of this file.
We tried to use an
abbreviation instead of a
notation but this led to hard-to-debug elaboration
errors. So, we introduce a localized notation instead. When this notation is enabled with
open Affine, Lean will use
AffineSpace instead of
AddTorsor both in input and in the
Here is an incomplete list of notions related to affine spaces, all of them are defined in other files:
AffineMap: a map between affine spaces that preserves the affine structure;
AffineEquiv: an equivalence between affine spaces that preserves the affine structure;
AffineSubspace: a subset of an affine space closed w.r.t. affine combinations of points;
AffineCombination: an affine combination of points;
AffineIndependent: affine independent set of points;
AffineBasis.coord: the barycentric coordinate of a point.
Some key definitions are not yet present.
- Affine frames. An affine frame might perhaps be represented as an
Finsupp(in the general case) or function type (in the finite-dimensional case) that gives the coordinates, with appropriate proofs of existence when
kis a field.