Commit 2024-02-06 17:35 8e0aa131

View on Github →

fix: improvements I noticed when teaching (#8420)

  • Rename (and generalize and move)
Int.units_ne_neg_self -> units_ne_neg_self
Int.neg_units_ne_self -> neg_units_ne_self
  • Change the simps config for Closeds
  • Add some gcongr-lemmas (currently is a bit picky about the exact statement of lemmas tagged with gcongr, so I had to add some variants that I could tag).

Estimated changes

added theorem neg_units_ne_self
added theorem units_ne_neg_self
deleted theorem Int.neg_units_ne_self
deleted theorem Int.units_ne_neg_self
added theorem Filter.comap_le_comap
added theorem Filter.map_le_map