Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 05:18 a370cf05

View on Github →

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

  • rename set.mem_Ioo_or_eq_endpoints_of_mem_Iccset.eq_endpoints_or_mem_Ioo_of_mem_Icc;
  • rename set.mem_Ioo_or_eq_left_of_mem_Icoset.eq_left_or_mem_Ioo_of_mem_Ico;
  • rename set.mem_Ioo_or_eq_right_of_mem_Iocset.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.

Estimated changes