Commit 2022-10-11 21:54 0a0be05e

View on Github →

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

Estimated changes

Modified src/data/set/intervals/unordered_interval.lean

added theorem set.eq_of_mem_interval_oc_of_mem_interval_oc'

added theorem set.eq_of_mem_interval_oc_of_mem_interval_oc

added theorem set.eq_of_mem_interval_of_mem_interval'

added theorem set.eq_of_mem_interval_of_mem_interval

added theorem set.eq_of_not_mem_interval_oc_of_not_mem_interval_oc

added theorem set.interval_eq_union

added theorem set.interval_injective_left

added theorem set.interval_injective_right

added theorem set.interval_oc_injective_left

added theorem set.interval_oc_injective_right

modified theorem set.interval_oc_of_le

modified theorem set.interval_oc_of_lt

modified theorem set.left_mem_interval

added theorem set.left_mem_interval_oc

added theorem set.mem_interval

added theorem set.mem_interval_oc

added theorem set.not_mem_interval_oc

modified theorem set.not_mem_interval_of_gt

modified theorem set.not_mem_interval_of_lt

modified theorem set.right_mem_interval

added theorem set.right_mem_interval_oc