Commit 2022-06-14 13:35 5d18a722

View on Github →

feat(order/{conditionally_complete_lattice,galois_connection): Supremum of set.image2 (#14307) Sup and Inf distribute over set.image2 in the presence of appropriate Galois connections.

Estimated changes

Modified src/order/complete_lattice.lean

added theorem Inf_image2

added theorem Sup_image2

added theorem binfi_prod

added theorem bsupr_prod

modified theorem infi_prod

modified theorem supr_prod

Modified src/order/conditionally_complete_lattice.lean

added theorem cInf_image2_eq_cInf_cInf

added theorem cInf_image2_eq_cInf_cSup

added theorem cInf_image2_eq_cSup_cInf

added theorem cInf_image2_eq_cSup_cSup

added theorem cSup_image2_eq_cInf_cInf

added theorem cSup_image2_eq_cInf_cSup

added theorem cSup_image2_eq_cSup_cInf

added theorem cSup_image2_eq_cSup_cSup

added theorem csupr_le_iff

added theorem csupr_set_le_iff

added theorem le_cinfi_iff

added theorem le_cinfi_set_iff

Modified src/order/galois_connection.lean

added theorem Inf_image2_eq_Inf_Inf

added theorem Inf_image2_eq_Inf_Sup

added theorem Inf_image2_eq_Sup_Inf

added theorem Inf_image2_eq_Sup_Sup

added theorem Sup_image2_eq_Inf_Inf

added theorem Sup_image2_eq_Inf_Sup

added theorem Sup_image2_eq_Sup_Inf

added theorem Sup_image2_eq_Sup_Sup