Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 17:56 3a0b0d1d

View on Github →

chore(order/lattice): add exists_lt_of_sup/inf (#10133)

Estimated changes

added theorem exists_lt_of_inf
added theorem exists_lt_of_sup