Commit 2022-12-06 22:18 6981386d

View on Github →

chore: tidy Order.Hom.Basic (#889)

Estimated changes

Modified Mathlib/Order/Hom/Basic.lean

added theorem Codisjoint.map_orderIso

deleted theorem Codisjoint.map_order_iso

added theorem Disjoint.map_orderIso

deleted theorem Disjoint.map_order_iso

added theorem OrderEmbedding.coe_ofMapLeIff

deleted theorem OrderEmbedding.coe_of_map_le_iff

added theorem OrderIso.coe_dualDual

added theorem OrderIso.coe_dualDual_symm

deleted theorem OrderIso.coe_dual_dual

deleted theorem OrderIso.coe_dual_dual_symm

added theorem OrderIso.coe_prodComm

deleted theorem OrderIso.coe_prod_comm

added theorem OrderIso.coe_toOrderEmbedding

deleted theorem OrderIso.coe_to_order_embedding

added theorem OrderIso.complementedLattice

added theorem OrderIso.complementedLattice_iff

deleted theorem OrderIso.complemented_lattice

deleted theorem OrderIso.complemented_lattice_iff

added theorem OrderIso.dualDual_apply

added theorem OrderIso.dualDual_symm_apply

deleted theorem OrderIso.dual_dual_apply

deleted theorem OrderIso.dual_dual_symm_apply

added theorem OrderIso.funUnique_symm_apply

deleted theorem OrderIso.fun_unique_symm_apply

added theorem OrderIso.prodComm_symm

deleted theorem OrderIso.prod_comm_symm

added theorem OrderIso.refl_toEquiv

deleted theorem OrderIso.refl_to_equiv

added theorem OrderIso.toEquiv_symm

added theorem OrderIso.toFun_eq_coe

deleted theorem OrderIso.to_equiv_symm

deleted theorem OrderIso.to_fun_eq_coe

added theorem WithTop.coe_toDualBotEquiv

deleted theorem WithTop.coe_to_dualBotEquiv_eq

added theorem codisjoint_map_orderIso_iff

deleted theorem codisjoint_map_order_iso_iff

added theorem disjoint_map_orderIso_iff

deleted theorem disjoint_map_order_iso_iff