unordered_interval): Intervals are injective in both endpoints (#16168)

Commit

3 years ago

feat(data/set/intervals/unordered_interval): Intervals are injective in both endpoints (#16168) `set.interval a` and `set.interval_oc a` are injective.

Author

YaelDillies

Parents

93def16e

mathlib3 0a0be05e - feat(data/set/intervals/unordered_interval): Intervals are injective in both endpoints (#16168)

mathlib3
0a0be05e - feat(data/set/intervals/unordered_interval): Intervals are injective in both endpoints (#16168)