Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-10-06 08:03
e52e5338
View on Github →
feat(order/bounds): Antitone lemmas (
#9556
)
Estimated changes
Modified
src/order/bounds.lean
added
theorem
antitone.image_lower_bounds_subset_upper_bounds_image
added
theorem
antitone.image_upper_bounds_subset_lower_bounds_image
added
theorem
antitone.is_lub_image_le
added
theorem
antitone.le_is_glb_image
added
theorem
antitone.map_bdd_above
added
theorem
antitone.map_bdd_below
added
theorem
antitone.map_is_greatest
added
theorem
antitone.map_is_least
added
theorem
antitone.mem_lower_bounds_image
added
theorem
antitone.mem_upper_bounds_image