Commit 2022-12-06 03:48 56b03ee0

View on Github →

feat: port Order.Hom.Basic (#804) mathlib3 git sha 62a5626868683c104774de8d85b9855234ac807c

depends on: #772
depends on: #838

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Relation.lean

Modified Mathlib/Order/BooleanAlgebra.lean

Modified Mathlib/Order/Compare.lean

Created Mathlib/Order/Hom/Basic.lean

added theorem Codisjoint.map_order_iso

added theorem Disjoint.map_order_iso

added theorem Equiv.coe_toOrderIso

added def Equiv.toOrderIso

added theorem Equiv.toOrderIso_toEquiv

added theorem OrderEmbedding.coe_ofStrictMono

added theorem OrderEmbedding.coe_of_map_le_iff

added theorem OrderEmbedding.eq_iff_eq

added theorem OrderEmbedding.le_iff_le

added theorem OrderEmbedding.le_map_sup

added def OrderEmbedding.ltEmbedding

added theorem OrderEmbedding.lt_embedding_apply

added theorem OrderEmbedding.lt_iff_lt

added theorem OrderEmbedding.map_inf_le

added def OrderEmbedding.ofMapLeIff

added def OrderEmbedding.ofStrictMono

added def OrderEmbedding.subtype

added def OrderEmbedding.toOrderHom

added def OrderHom.Subtype.val

added def OrderHom.apply

added theorem OrderHom.apply_mono

added def OrderHom.coeFnHom

added theorem OrderHom.coe_copy

added theorem OrderHom.coe_fun_mk

added theorem OrderHom.coe_le_coe

added def OrderHom.comp

added theorem OrderHom.comp_const

added theorem OrderHom.comp_id

added theorem OrderHom.comp_mono

added theorem OrderHom.comp_prod_comp_same

added def OrderHom.compₘ

added def OrderHom.const

added theorem OrderHom.const_comp

added theorem OrderHom.copy_eq

added def OrderHom.curry

added theorem OrderHom.curry_apply

added theorem OrderHom.curry_symm_apply

added def OrderHom.diag

added def OrderHom.dualIso

added theorem OrderHom.dual_comp

added theorem OrderHom.dual_id

added theorem OrderHom.ext

added def OrderHom.fst

added theorem OrderHom.fst_comp_prod

added theorem OrderHom.fst_prod_snd

added def OrderHom.id

added theorem OrderHom.id_comp

added theorem OrderHom.le_def

added theorem OrderHom.mk_le_mk

added def OrderHom.onDiag

added theorem OrderHom.order_hom_eq_id

added def OrderHom.pi

added def OrderHom.piIso

added def OrderHom.prodIso

added def OrderHom.prodMap

added theorem OrderHom.prod_mono

added def OrderHom.prodₘ

added def OrderHom.snd

added theorem OrderHom.snd_comp_prod

added theorem OrderHom.symm_dual_comp

added theorem OrderHom.symm_dual_id

added structure OrderHom

added theorem OrderIso.apply_eq_iff_eq

added theorem OrderIso.apply_eq_iff_eq_symm_apply

added theorem OrderIso.apply_symm_apply

added theorem OrderIso.coe_dual_dual

added theorem OrderIso.coe_dual_dual_symm

added theorem OrderIso.coe_prod_comm

added theorem OrderIso.coe_refl

added theorem OrderIso.coe_to_order_embedding

added theorem OrderIso.coe_trans

added theorem OrderIso.complemented_lattice

added theorem OrderIso.complemented_lattice_iff

added def OrderIso.dualDual

added theorem OrderIso.dual_dual_apply

added theorem OrderIso.dual_dual_symm_apply

added theorem OrderIso.ext

added def OrderIso.funUnique

added theorem OrderIso.fun_unique_symm_apply

added theorem OrderIso.isCompl

added theorem OrderIso.isCompl_iff

added theorem OrderIso.le_iff_le

added theorem OrderIso.le_symm_apply

added theorem OrderIso.lt_iff_lt

added theorem OrderIso.map_bot'

added theorem OrderIso.map_bot

added theorem OrderIso.map_inf

added theorem OrderIso.map_sup

added theorem OrderIso.map_top'

added theorem OrderIso.map_top

added def OrderIso.ofCmpEqCmp

added def OrderIso.ofHomInv

added def OrderIso.ofRelIsoLT

added theorem OrderIso.ofRelIsoLT_apply

added theorem OrderIso.ofRelIsoLT_symm

added theorem OrderIso.ofRelIsoLT_toRelIsoLT

added def OrderIso.prodComm

added theorem OrderIso.prod_comm_symm

added def OrderIso.refl

added theorem OrderIso.refl_apply

added theorem OrderIso.refl_to_equiv

added theorem OrderIso.refl_trans

added def OrderIso.symm

added theorem OrderIso.symm_apply_apply

added theorem OrderIso.symm_apply_eq

added theorem OrderIso.symm_apply_le

added theorem OrderIso.symm_injective

added theorem OrderIso.symm_refl

added theorem OrderIso.symm_symm

added theorem OrderIso.symm_trans

added theorem OrderIso.symm_trans_apply

added def OrderIso.toOrderEmbedding

added def OrderIso.toRelIsoLT

added theorem OrderIso.toRelIsoLT_apply

added theorem OrderIso.toRelIsoLT_ofRelIsoLT

added theorem OrderIso.toRelIsoLT_symm

added theorem OrderIso.to_equiv_symm

added theorem OrderIso.to_fun_eq_coe

added def OrderIso.trans

added theorem OrderIso.trans_apply

added theorem OrderIso.trans_refl

added def OrderIso.withBotCongr

added theorem OrderIso.withBotCongr_refl

added theorem OrderIso.withBotCongr_symm

added theorem OrderIso.withBotCongr_trans

added def OrderIso.withTopCongr

added theorem OrderIso.withTopCongr_refl

added theorem OrderIso.withTopCongr_symm

added theorem OrderIso.withTopCongr_trans

added def Pi.evalOrderHom

added def RelEmbedding.orderEmbeddingOfLtEmbedding

added theorem RelEmbedding.order_embedding_of_lt_embedding_apply

added theorem RelEmbedding.toOrderHom_injective

added def RelHom.toOrderHom

added def StrictMono.orderIsoOfRightInverse

added theorem WithBot.coe_toDualTopEquiv_eq

added theorem WithBot.toDualTopEquiv_bot

added theorem WithBot.toDualTopEquiv_coe

added theorem WithBot.toDualTopEquiv_symm_bot

added theorem WithBot.toDualTopEquiv_symm_coe

added theorem WithTop.coe_to_dualBotEquiv_eq

added theorem WithTop.toDualBotEquiv_coe

added theorem WithTop.toDualBotEquiv_symm_coe

added theorem WithTop.toDualBotEquiv_symm_top

added theorem WithTop.toDualBotEquiv_top

added theorem codisjoint_map_order_iso_iff

added theorem disjoint_map_order_iso_iff

added theorem le_map_inv_iff

added theorem lt_map_inv_iff

added theorem map_inv_le_iff

added theorem map_inv_lt_iff

added theorem map_lt_map_iff

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/Order/WithBot.lean

Modified Mathlib/Tactic/ApplyFun.lean

Modified Mathlib/Tactic/Coe.lean

Modified Mathlib/Tactic/Simps/Basic.lean