Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-12 16:16 357b2966

View on Github →

feat(analysis/convex/side): betweenness and affine subspaces (#16733) 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.

Estimated changes

added theorem wbtw.w_opp_side₁₃
added theorem wbtw.w_opp_side₃₁
added theorem wbtw.w_same_side₁₂
added theorem wbtw.w_same_side₂₁
added theorem wbtw.w_same_side₂₃
added theorem wbtw.w_same_side₃₂