feat(analysis/convex/side): betweenness and affine subspaces (#16733) · leanprover-community/mathlib3@357b296 · GitHub

This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

feat(analysis/convex/side): betweenness and affine subspaces (#16733)

Browse files

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.

Loading branch information

jsm28 committed Oct 12, 2022

1 parent b49d568 commit 357b296