Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 21:33 7181b3af

View on Github →

chore(order/hom): rearrange definitions of order_{hom,iso,embedding} (#10752) We symmetrize the locations of rel_{hom,iso,embedding} and order_{hom,iso,embedding} by putting the rel_ definitions in order/rel_iso.lean and the order_ definitions in order/hom/basic.lean. (order_hom.lean needed to be split up to fix an import loop.) Requested by @YaelDillies.

Moved definitions

  • order_hom, order_iso, order_embedding are now in order/hom/basic.lean
  • order_hom.has_sup ... order_hom.complete_lattice are now in order/hom/lattice.lean

Other changes

Some import cleanup.

Estimated changes

added theorem disjoint.map_order_iso
added theorem equiv.coe_to_order_iso
added def order_embedding
added def order_hom.apply
added theorem order_hom.apply_mono
added theorem order_hom.coe_fun_mk
added theorem order_hom.coe_le_coe
added def order_hom.comp
added theorem order_hom.comp_const
added theorem order_hom.comp_id
added theorem order_hom.comp_mono
added def order_hom.const
added theorem order_hom.const_comp
added def order_hom.curry
added theorem order_hom.curry_apply
added def order_hom.diag
added theorem order_hom.ext
added def order_hom.fst
added theorem order_hom.fst_prod_snd
added def order_hom.id
added theorem order_hom.id_comp
added theorem order_hom.le_def
added theorem order_hom.mk_le_mk
added def order_hom.pi
added def order_hom.pi_iso
added theorem order_hom.prod_mono
added def order_hom.snd
added def order_hom.unique
added structure order_hom
added theorem order_iso.coe_refl
added theorem order_iso.coe_trans
added theorem order_iso.is_compl
added theorem order_iso.is_compl_iff
added theorem order_iso.le_iff_le
added theorem order_iso.lt_iff_lt
added theorem order_iso.map_bot'
added theorem order_iso.map_bot
added theorem order_iso.map_inf
added theorem order_iso.map_sup
added theorem order_iso.map_top'
added theorem order_iso.map_top
added theorem order_iso.range_eq
added def order_iso.refl
added theorem order_iso.refl_apply
added theorem order_iso.refl_trans
added def order_iso.symm
added theorem order_iso.symm_refl
added theorem order_iso.symm_symm
added def order_iso.trans
added theorem order_iso.trans_apply
added theorem order_iso.trans_refl
added def order_iso
added theorem order_hom.Inf_apply
added theorem order_hom.Sup_apply
added theorem order_hom.coe_infi
added theorem order_hom.coe_supr
added theorem order_hom.infi_apply
added theorem order_hom.supr_apply
deleted theorem order_hom.Inf_apply
deleted theorem order_hom.Sup_apply
deleted def order_hom.apply
deleted theorem order_hom.apply_mono
deleted theorem order_hom.coe_fun_mk
deleted theorem order_hom.coe_infi
deleted theorem order_hom.coe_le_coe
deleted theorem order_hom.coe_supr
deleted def order_hom.comp
deleted theorem order_hom.comp_const
deleted theorem order_hom.comp_id
deleted theorem order_hom.comp_mono
deleted def order_hom.compₘ
deleted def order_hom.const
deleted theorem order_hom.const_comp
deleted def order_hom.curry
deleted theorem order_hom.curry_apply
deleted def order_hom.diag
deleted def order_hom.dual_iso
deleted theorem order_hom.ext
deleted def order_hom.fst
deleted theorem order_hom.fst_comp_prod
deleted theorem order_hom.fst_prod_snd
deleted def order_hom.id
deleted theorem order_hom.id_comp
deleted theorem order_hom.infi_apply
deleted theorem order_hom.le_def
deleted theorem order_hom.mk_le_mk
deleted def order_hom.on_diag
deleted theorem order_hom.order_hom_eq_id
deleted def order_hom.pi
deleted def order_hom.pi_iso
deleted def order_hom.prod_iso
deleted def order_hom.prod_map
deleted theorem order_hom.prod_mono
deleted def order_hom.prodₘ
deleted def order_hom.snd
deleted theorem order_hom.snd_comp_prod
deleted theorem order_hom.supr_apply
deleted theorem order_hom.to_fun_eq_coe
deleted def order_hom.unique
deleted structure order_hom
deleted def pi.eval_order_hom
deleted theorem disjoint.map_order_iso
deleted theorem equiv.coe_to_order_iso
deleted def equiv.to_order_iso
deleted theorem order_embedding.eq_iff_eq
deleted theorem order_embedding.le_iff_le
deleted theorem order_embedding.lt_iff_lt
deleted def order_embedding
deleted theorem order_iso.apply_eq_iff_eq
deleted theorem order_iso.coe_refl
deleted theorem order_iso.coe_trans
deleted theorem order_iso.image_preimage
deleted theorem order_iso.is_compl
deleted theorem order_iso.is_compl_iff
deleted theorem order_iso.is_complemented
deleted theorem order_iso.le_iff_le
deleted theorem order_iso.le_symm_apply
deleted theorem order_iso.lt_iff_lt
deleted theorem order_iso.map_bot'
deleted theorem order_iso.map_bot
deleted theorem order_iso.map_inf
deleted theorem order_iso.map_sup
deleted theorem order_iso.map_top'
deleted theorem order_iso.map_top
deleted theorem order_iso.preimage_image
deleted theorem order_iso.range_eq
deleted def order_iso.refl
deleted theorem order_iso.refl_apply
deleted theorem order_iso.refl_to_equiv
deleted theorem order_iso.refl_trans
deleted def order_iso.set.univ
deleted def order_iso.set_congr
deleted def order_iso.symm
deleted theorem order_iso.symm_apply_eq
deleted theorem order_iso.symm_apply_le
deleted theorem order_iso.symm_injective
deleted theorem order_iso.symm_refl
deleted theorem order_iso.symm_symm
deleted theorem order_iso.to_equiv_symm
deleted def order_iso.trans
deleted theorem order_iso.trans_apply
deleted theorem order_iso.trans_refl
deleted def order_iso