Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:31 d359aa89

View on Github →

feat(order/conditionally_complete_lattice): cinfi_const (#634)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.range_const

Modified src/order/conditionally_complete_lattice.lean

added theorem lattice.cinfi_const

modified theorem lattice.cinfi_le

added theorem lattice.csupr_const

modified theorem lattice.le_csupr