mathlib3
a370cf05 - chore(data/set/intervals): golf, rename (#12893)

Commit
3 years ago
chore(data/set/intervals): golf, rename (#12893) * rename `set.mem_Ioo_or_eq_endpoints_of_mem_Icc` → `set.eq_endpoints_or_mem_Ioo_of_mem_Icc`; * rename `set.mem_Ioo_or_eq_left_of_mem_Ico` → `set.eq_left_or_mem_Ioo_of_mem_Ico`; * rename `set.mem_Ioo_or_eq_right_of_mem_Ioc` → `set.eq_right_or_mem_Ioo_of_mem_Ioc`; * golf the proofs of these lemmas. The new names better reflect the order of terms in `or`.
Author
Parents
Loading