Commit 2023-11-03 09:34 b3e4ef91

View on Github →

feat(Order/PartialSups): golf, add lemmas (#8138)

  • Add partialSups_iff_forall and partialSups_le_iff.
  • Use them to golf some proofs.
  • Drop partialSups_apply_mono because it's just (partialSups f).mono.
  • Add disjoint_partialSups_left and disjoint_partialSups_right. Motivated by partialSups_le_iff from the Mandelbrot Set Connectedness Project.

Estimated changes

modified theorem le_partialSups_of_le
deleted theorem partialSups_apply_mono
modified theorem partialSups_eq_ciSup_Iic
added theorem partialSups_iff_forall
added theorem partialSups_le_iff
modified theorem partialSups_mono