Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 12:55 29ad1c8f

View on Github →

feat(order/complete_lattice): add rewrite rules for Inf/Sup/infi/supr for pi and Prop

Estimated changes

added theorem lattice.Inf_Prop_eq
added theorem lattice.Inf_apply
added theorem lattice.Sup_Prop_eq
added theorem lattice.Sup_apply
added theorem lattice.infi_Prop_eq
added theorem lattice.infi_apply
added theorem lattice.supr_Prop_eq
added theorem lattice.supr_apply