Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-13 18:45 3e78b858

View on Github →

refactor(order/complete_lattice): make supr and infi available in has_Sup and has_Inf (#472)

Estimated changes

Modified linear_algebra/lc.lean

Modified order/complete_lattice.lean

modified def lattice.infi

modified theorem lattice.infi_congr_Prop

modified def lattice.supr

modified theorem lattice.supr_congr_Prop