Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 20:53 164690af

View on Github →

feat(analysis/convex/between): more transitivity variants (#17527) Add more variants of transitivity lemmas, giving that one endpoint is not equal to the middle point in cases where the hypotheses imply weak betweenness (and we already have the corresponding transitivity lemmas for that), and that one endpoint is not equal to the middle point, but don't imply strict betweenness.

Estimated changes