Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-18 13:20 6b6b04ac

View on Github →

feat(order/complete_lattice): add rules for supr/infi under image and under propositions

Estimated changes

added theorem lattice.infi_eq_dif
added theorem lattice.infi_eq_if
added theorem lattice.infi_image
added theorem lattice.supr_eq_dif
added theorem lattice.supr_eq_if
added theorem lattice.supr_image