[Merged by Bors] - feat(analysis/convex/side): betweenness and affine subspaces #16733
Conversation
Define notions of points being (weakly or strictly) on the same side or opposite sides of an affine subspace (e.g. a line), for use in describing geometrical configurations, and provide some associated API.
src/analysis/convex/between.lean
Outdated
| @@ -9,13 +9,22 @@ import linear_algebra.affine_space.finite_dimensional | |||
| /-! | |||
| # Betweenness in affine spaces | |||
|
|
|||
| This file defines notions of a point in an affine space being between two given points. | |||
| This file defines notions of a point in an affine space being between two given points, and of | |||
| two points being on the same or opposite sides of an affine subspace. | |||
|
|
|||
| ## Main definitions | |||
|
|
|||
| * `affine_segment R x y`: The segment of points weakly between `x` and `y`. | |||
| * `wbtw R x y z`: The point `y` is weakly between `x` and `z`. | |||
There was a problem hiding this comment.
Is it helpful to use mathlib's btw in this file, or is that less convenient?
There was a problem hiding this comment.
I don't think the btw used in circular orders is suitable for betweenness in affine spaces, because modules and affine spaces take the ring as an explicit parameter, not an out_param, so that there can be multiple module structures with different rings on the same type, so there isn't a canonical betweenness relation on a given type of points without specifying the ring as an explicit parameter to that relation.
(I have figured out how to use mathlib's circular orders for defining an explicit concept of cyclic polygons, which wasn't initially clear: a canonical cyclic order can be defined on a quotient of an archimedean linear_ordered_add_comm_group, and a notion can be defined of a cycle in a cyclic order being (strictly or weakly) in (positive) cyclic order; applying that to real.angle gives notions of positively and negatively cyclic polygons in an oriented two-dimensional Euclidean affine space, from which notions of cyclic polygons without a sign specified can be deduced in any Euclidean affine space without needing an orientation or a restriction to two dimensions.)
|
Would it make sense to start a new file called |
jsm28
changed the title
leanprover-community-bot-assistant
added
delegated
|
✌️ jsm28 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Define notions of points being (weakly or strictly) on the same side or opposite sides of an affine subspace (e.g. a line), for use in describing geometrical configurations, and provide some associated API.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Define notions of points being (weakly or strictly) on the same side or opposite sides of an affine subspace (e.g. a line), for use in describing geometrical configurations, and provide some associated API.