Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-03 17:55 9d129dc2

View on Github →

feat(algebra/bounds): a few lemmas like bdd_above (-s) ↔ bdd_below s (#8522)

Estimated changes

added theorem bdd_above.inv
added theorem bdd_above.mul
added theorem bdd_above_inv
added theorem bdd_below.inv
added theorem bdd_below.mul
added theorem bdd_below_inv
added theorem is_glb.inv
added theorem is_glb_inv'
added theorem is_glb_inv
added theorem is_lub.inv
added theorem is_lub_inv'
added theorem is_lub_inv