Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-26 09:03 33df7e88

View on Github →

feat(order/conditionally_complete_lattice): with_top (with_bot L) ins… (#1725)

  • feat(order/conditionally_complete_lattice): with_top (with_bot L) instances
  • dealing with most of Sebastien's comments
  • initial defs. Now what happens?
  • half way there
  • compiles!
  • tidy
  • removing dead code
  • docstring tinkering
  • removing unused code
  • is_lub_Sup' added
  • refactor final proofs
  • conforming to mathlib conventions
  • def -> lemma

Estimated changes