Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 12:59 a2d7b55a

View on Github →

feat(order/complete_boolean_algebra): Frames (#11709) Define the order theoretic order.frame and order.coframe and insert them between complete_lattice and complete_distrib_lattice.

Estimated changes

modified theorem Sup_inf_Sup
modified theorem Sup_inf_eq
added theorem binfi_sup_binfi
added theorem bsupr_inf_bsupr
modified theorem bsupr_inf_eq
modified theorem inf_Sup_eq
modified theorem inf_bsupr_eq
modified theorem inf_supr_eq
added theorem infi_sup_infi
modified theorem supr_inf_eq
added theorem supr_inf_supr