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 justmem_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 arguments ⊆ t
from the following (the old theorems follow immediately from the new ones andmonotone_on.mono
):monotone_on.map_is_greatest
monotone_on.map_is_least
antitone_on.map_is_greatest
antitone_on.map_is_least