Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-30 19:55 c034b4c2

View on Github →

chore(order/bounds): +2 lemmas, fix a name (#2877)

Estimated changes

Modified src/order/bounds.lean

added theorem mem_lower_bounds

added theorem mem_upper_bounds

added theorem monotone.le_is_glb_image

deleted theorem monotone.le_is_glb_image_le