Commit 2023-01-02 16:54 625deea9

View on Github →

feat: port Data.Int.ConditionallyCompleteOrder (#1299)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/ConditionallyCompleteOrder.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