Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-03 11:13 3f4b8368

View on Github →

feat(order/bounds): add is_lub_pi and is_glb_pi (#8521)

Estimated changes

Modified src/order/basic.lean

added theorem function.monotone_eval

Modified src/order/bounds.lean

added theorem is_glb_pi

added theorem is_lub_pi