Commit 2025-12-28 19:10 b9b7d0ba

View on Github →

refactor(Order/Interval/Set/Basic): review some basic Ixx theorems (#33328) This PR does the following:

  • Deprecate various lemmas of the form x ∈ Ixx a b ↔ False in favor of new lemmas x ∉ Ixx a b.
  • Rename lemmas left_mem_Ixi and right_mem_Iix to simply self_mem_Ixi or self_mem_Iix.

Estimated changes

modified theorem Set.left_mem_Icc
deleted theorem Set.left_mem_Ici
modified theorem Set.left_mem_Ico
added theorem Set.left_notMem_Ioc
added theorem Set.left_notMem_Ioo
modified theorem Set.right_mem_Icc
deleted theorem Set.right_mem_Iic
modified theorem Set.right_mem_Ioc
added theorem Set.right_notMem_Ico
added theorem Set.right_notMem_Ioo
added theorem Set.self_mem_Ici
added theorem Set.self_mem_Iic
added theorem Set.self_notMem_Iio
added theorem Set.self_notMem_Ioi