Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 19:44 57f382a0

View on Github →

feat(order/bounds): Boundedness of monotone/antitone functions (#13079)

Estimated changes

Modified src/order/bounds.lean

added theorem antitone_on.image_lower_bounds_subset_upper_bounds_image

added theorem antitone_on.image_upper_bounds_subset_lower_bounds_image

added theorem antitone_on.is_lub_image_le

added theorem antitone_on.le_is_glb_image

added theorem antitone_on.map_bdd_above

added theorem antitone_on.map_bdd_below

added theorem antitone_on.map_is_greatest

added theorem antitone_on.map_is_least

added theorem antitone_on.mem_lower_bounds_image

added theorem antitone_on.mem_upper_bounds_image

added theorem monotone_on.image_lower_bounds_subset_lower_bounds_image

added theorem monotone_on.image_upper_bounds_subset_upper_bounds_image

added theorem monotone_on.is_lub_image_le

added theorem monotone_on.le_is_glb_image

added theorem monotone_on.map_bdd_above

added theorem monotone_on.map_bdd_below

added theorem monotone_on.map_is_greatest

added theorem monotone_on.map_is_least

added theorem monotone_on.mem_lower_bounds_image

added theorem monotone_on.mem_upper_bounds_image