Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-17 13:27 ff716d24

View on Github →

chore(order/bounds): golf (#5401)

Estimated changes

Modified src/order/bounds.lean

added theorem is_glb.exists_between'

added theorem is_glb.exists_between

modified theorem is_glb.exists_between_self_add'

modified theorem is_glb.exists_between_self_add

added theorem is_lub.exists_between'

added theorem is_lub.exists_between

modified theorem is_lub.exists_between_sub_self'

modified theorem is_lub.exists_between_sub_self

Modified src/topology/instances/real.lean