Commit 2021-07-13 21:48 5021c1f9

View on Github →

feat(data/int): conditionally complete linear order (#8149) Prove that the integers form a conditionally complete linear order. I do not have a specific goal in mind for this, but it would have been helpful to formulate one of the Proof Ground problems using this.

Estimated changes

Modified src/data/int/basic.lean

added theorem int.coe_greatest_of_bdd_eq

added theorem int.coe_least_of_bdd_eq

Created src/data/int/order.lean

added theorem int.cInf_empty

added theorem int.cInf_eq_least_of_bdd

added theorem int.cInf_mem

added theorem int.cInf_of_not_bdd_below

added theorem int.cSup_empty

added theorem int.cSup_eq_greatest_of_bdd

added theorem int.cSup_mem

added theorem int.cSup_of_not_bdd_above