Affine space #
In this file we introduce the following notation:
affine_space V Pis an alternative notation for
add_torsor 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_locale affine, Lean will use
affine_space instead of
add_torsor 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:
affine_map: a map between affine spaces that preserves the affine structure;
affine_equiv: an equivalence between affine spaces that preserves the affine structure;
affine_subspace: a subset of an affine space closed w.r.t. affine combinations of points;
affine_combination: an affine combination of points;
affine_independent: affine independent set of points;
affine_basis.coord: the barycentric coordinate of a point.
Some key definitions are not yet present.