Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 10:36 086469f7

View on Github →

chore(order/*): Change order_hom notation (#10988) This changes the notation for order_hom from α →ₘ β to α →o β to match order_embedding and order_iso, which are respectively α ↪o β and α ≃o β. This also solves the conflict with measurable functions.

Estimated changes

modified def mul_roth_number
modified def roth_number_nat
modified theorem part.to_unit_cont
modified def part.to_unit_mono
modified def finset.erase_none
modified theorem submodule.coe_supr_of_chain
modified theorem submodule.mem_supr_of_chain
modified def linear_map.tunnel
modified structure closure_operator
modified def order_hom.gfp
modified theorem order_hom.gfp_gfp
modified def order_hom.lfp
modified theorem order_hom.lfp_lfp
modified def order_hom.apply
modified theorem order_hom.apply_mono
modified def order_hom.coe_fn_hom
modified theorem order_hom.coe_le_coe
modified def order_hom.comp
modified theorem order_hom.comp_const
modified theorem order_hom.comp_id
modified theorem order_hom.comp_mono
modified def order_hom.compₘ
modified def order_hom.const
modified theorem order_hom.const_comp
modified def order_hom.curry
modified theorem order_hom.curry_apply
modified theorem order_hom.curry_symm_apply
modified def order_hom.diag
modified theorem order_hom.ext
modified def order_hom.fst
modified theorem order_hom.fst_comp_prod
modified theorem order_hom.fst_prod_snd
modified def order_hom.id
modified theorem order_hom.id_comp
modified theorem order_hom.le_def
modified def order_hom.on_diag
modified theorem order_hom.order_hom_eq_id
modified def order_hom.pi
modified def order_hom.pi_iso
modified def order_hom.prod_iso
modified def order_hom.prod_map
modified theorem order_hom.prod_mono
modified def order_hom.prodₘ
modified def order_hom.snd
modified theorem order_hom.snd_comp_prod
modified def order_hom.subtype.val
modified theorem order_hom.to_fun_eq_coe
modified def order_hom.unique
modified def pi.eval_order_hom
modified def rel_hom.to_order_hom
modified theorem order_hom.Inf_apply
modified theorem order_hom.Sup_apply
modified theorem order_hom.coe_infi
modified theorem order_hom.coe_supr
modified theorem order_hom.infi_apply
modified theorem order_hom.supr_apply
modified def order_hom.bind
modified def partial_sups.gi
modified def partial_sups
modified theorem partial_sups_mono