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 docs/references.bib

Modified src/data/set/prod.lean

added theorem set.image_prod_mk_subset_prod_left

added theorem set.image_prod_mk_subset_prod_right

Modified src/order/complete_boolean_algebra.lean

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

Modified src/order/copy.lean

added def coframe.copy

added def frame.copy