Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-05 18:50 93bc7e05

View on Github →

feat(order): add some missing pi and Prop instances (#7268)

Estimated changes

Modified src/order/boolean_algebra.lean

Modified src/order/bounded_lattice.lean

added theorem inf_Prop_eq

added theorem le_Prop_eq

deleted theorem le_iff_imp

added theorem sup_Prop_eq

Modified src/order/complete_boolean_algebra.lean

Modified src/order/complete_lattice.lean

modified theorem Inf_Prop_eq

modified theorem Sup_Prop_eq

modified theorem infi_Prop_eq

modified theorem infi_apply

modified theorem supr_Prop_eq

modified theorem supr_apply

added theorem supr_subtype''

Modified src/topology/omega_complete_partial_order.lean