Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 08:03 77110125

View on Github →

feat(order/hom/*): equivalences mapping morphisms to their dual (#12888) Add missing whatever_hom.dual equivalences.

Estimated changes

added theorem order_hom.dual_comp
added theorem order_hom.dual_id
added theorem order_hom.symm_dual_id
added theorem bot_hom.dual_comp
added theorem bot_hom.dual_id
added theorem bot_hom.symm_dual_comp
added theorem bot_hom.symm_dual_id
added theorem top_hom.dual_comp
added theorem top_hom.dual_id
added theorem top_hom.symm_dual_comp
added theorem top_hom.symm_dual_id
added theorem Inf_hom.dual_comp
added theorem Inf_hom.dual_id
added theorem Inf_hom.symm_dual_comp
added theorem Inf_hom.symm_dual_id
added theorem Sup_hom.dual_comp
added theorem Sup_hom.dual_id
added theorem Sup_hom.symm_dual_comp
added theorem Sup_hom.symm_dual_id
added theorem inf_hom.dual_comp
added theorem inf_hom.dual_id
added theorem inf_hom.symm_dual_comp
added theorem inf_hom.symm_dual_id
added theorem inf_top_hom.dual_comp
added theorem inf_top_hom.dual_id
added theorem lattice_hom.dual_comp
added theorem lattice_hom.dual_id
added def sup_bot_hom.dual
added theorem sup_bot_hom.dual_comp
added theorem sup_bot_hom.dual_id
added theorem sup_hom.dual_comp
added theorem sup_hom.dual_id
added theorem sup_hom.symm_dual_comp
added theorem sup_hom.symm_dual_id