Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-28 11:42 599240fc

View on Github →

refactor(order/bounds): general cleanup (#14127) Apart from golfing, this PR does the following: Add the following theorems (which are immediate from the non-self counterparts):

  • monotone_on.mem_upper_bounds_image_self
  • monotone_on.mem_lower_bounds_image_self
  • antitone_on.mem_upper_bounds_image_self
  • antitone_on.mem_lower_bounds_image_self Remove the following theorems (as they're just mem_X_bounds_image under unnecessarily stronger assumptions):
  • monotone_on.is_lub_image_le
  • monotone_on.le_is_glb_image
  • antitone_on.is_lub_image_le
  • antitone_on.le_is_glb_image
  • monotone.is_lub_image_le
  • monotone.le_is_glb_image
  • antitone.is_lub_image_le
  • antitone.le_is_glb_image Remove a redundant argument s ⊆ t from the following (the old theorems follow immediately from the new ones and monotone_on.mono):
  • monotone_on.map_is_greatest
  • monotone_on.map_is_least
  • antitone_on.map_is_greatest
  • antitone_on.map_is_least

Estimated changes

deleted theorem antitone.is_lub_image_le
deleted theorem antitone.le_is_glb_image
modified theorem antitone.map_bdd_above
modified theorem antitone.map_bdd_below
modified theorem antitone.map_is_greatest
modified theorem antitone.map_is_least
modified theorem antitone_on.map_is_greatest
modified theorem antitone_on.map_is_least
deleted theorem monotone.is_lub_image_le
deleted theorem monotone.le_is_glb_image
modified theorem monotone.map_bdd_above
modified theorem monotone.map_bdd_below
modified theorem monotone_on.map_is_greatest
modified theorem monotone_on.map_is_least