Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 03:16 ae8abf37

View on Github →

chore(order/rel_iso): rename order_iso and order_embedding to rel_iso and rel_embedding (#3750) renames order_iso and order_embedding, to make it clear they apply to all binary relations makes room for a new definition of order_embedding that will deal with order instances

Estimated changes

Modified scripts/nolints.txt

Modified src/data/equiv/encodable/basic.lean

Modified src/data/equiv/list.lean

Modified src/data/finsupp/lattice.lean

deleted def finsupp.order_embedding_to_fun

deleted theorem finsupp.order_embedding_to_fun_apply

deleted def finsupp.order_iso_multiset

deleted theorem finsupp.order_iso_multiset_apply

deleted theorem finsupp.order_iso_multiset_symm_apply

added def finsupp.rel_embedding_to_fun

added theorem finsupp.rel_embedding_to_fun_apply

added def finsupp.rel_iso_multiset

added theorem finsupp.rel_iso_multiset_apply

added theorem finsupp.rel_iso_multiset_symm_apply

Modified src/data/setoid/basic.lean

modified def setoid.correspondence

Modified src/data/setoid/partition.lean

deleted def setoid.partition.order_iso

added def setoid.partition.rel_iso

Modified src/group_theory/congruence.lean

modified def con.correspondence

Modified src/linear_algebra/basic.lean

deleted def submodule.comap_mkq.le_order_embedding

added def submodule.comap_mkq.le_rel_embedding

deleted def submodule.comap_mkq.lt_order_embedding

added def submodule.comap_mkq.lt_rel_embedding

deleted def submodule.comap_mkq.order_iso

added def submodule.comap_mkq.rel_iso

deleted def submodule.map_subtype.le_order_embedding

added def submodule.map_subtype.le_rel_embedding

deleted def submodule.map_subtype.lt_order_embedding

added def submodule.map_subtype.lt_rel_embedding

deleted def submodule.map_subtype.order_iso

added def submodule.map_subtype.rel_iso

Modified src/order/galois_connection.lean

deleted theorem order_iso.to_galois_connection

added theorem rel_iso.to_galois_connection

Modified src/order/ord_continuous.lean

deleted theorem left_ord_continuous.coe_to_le_order_embedding

added theorem left_ord_continuous.coe_to_le_rel_embedding

deleted theorem left_ord_continuous.coe_to_lt_order_embedding

added theorem left_ord_continuous.coe_to_lt_rel_embedding

deleted def left_ord_continuous.to_le_order_embedding

added def left_ord_continuous.to_le_rel_embedding

deleted def left_ord_continuous.to_lt_order_embedding

added def left_ord_continuous.to_lt_rel_embedding

deleted theorem right_ord_continuous.coe_to_le_order_embedding

added theorem right_ord_continuous.coe_to_le_rel_embedding

deleted theorem right_ord_continuous.coe_to_lt_order_embedding

added theorem right_ord_continuous.coe_to_lt_rel_embedding

deleted def right_ord_continuous.to_le_order_embedding

added def right_ord_continuous.to_le_rel_embedding

deleted def right_ord_continuous.to_lt_order_embedding

added def right_ord_continuous.to_lt_rel_embedding

Deleted src/order/order_iso.lean

deleted def fin.val.order_embedding

deleted def fin_fin.order_embedding

deleted theorem injective_of_increasing

deleted def order_embedding.cod_restrict

deleted theorem order_embedding.cod_restrict_apply

deleted theorem order_embedding.coe_fn_inj

deleted theorem order_embedding.coe_fn_mk

deleted theorem order_embedding.coe_fn_to_embedding

deleted theorem order_embedding.eq_preimage

deleted theorem order_embedding.injective

deleted theorem order_embedding.le_map_sup

deleted def order_embedding.lt_embedding_of_le_embedding

deleted theorem order_embedding.map_inf_le

deleted def order_embedding.of_monotone

deleted theorem order_embedding.of_monotone_coe

deleted theorem order_embedding.ord

deleted def order_embedding.preimage

deleted theorem order_embedding.refl_apply

deleted def order_embedding.rsymm

deleted theorem order_embedding.trans_apply

deleted structure order_embedding

deleted theorem order_iso.apply_inv_self

deleted theorem order_iso.apply_symm_apply

deleted theorem order_iso.coe_coe_fn

deleted theorem order_iso.coe_fn_injective

deleted theorem order_iso.coe_fn_mk

deleted theorem order_iso.coe_fn_symm_mk

deleted theorem order_iso.coe_fn_to_equiv

deleted theorem order_iso.coe_mul

deleted theorem order_iso.coe_one

deleted theorem order_iso.ext

deleted theorem order_iso.inv_apply_self

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.mul_apply

deleted theorem order_iso.of_surjective_coe

deleted theorem order_iso.ord''

deleted theorem order_iso.ord

deleted def order_iso.prod_lex_congr

deleted theorem order_iso.refl_apply

deleted theorem order_iso.rel_symm_apply

deleted def order_iso.rsymm

deleted def order_iso.sum_lex_congr

deleted theorem order_iso.symm_apply_apply

deleted theorem order_iso.symm_apply_rel

deleted theorem order_iso.to_equiv_injective

deleted def order_iso.to_order_embedding

deleted theorem order_iso.to_order_embedding_eq_coe

deleted theorem order_iso.trans_apply

deleted structure order_iso

deleted theorem preimage_equivalence

deleted def set_coe_embedding

deleted theorem subrel.order_embedding_apply

deleted def subrel

deleted theorem subrel_val

Modified src/order/order_iso_nat.lean

deleted def order_embedding.nat_gt

deleted def order_embedding.nat_lt

deleted theorem order_embedding.well_founded_iff_no_descending_seq

added def rel_embedding.nat_gt

added def rel_embedding.nat_lt

added theorem rel_embedding.well_founded_iff_no_descending_seq

Created src/order/rel_iso.lean

added def fin.val.rel_embedding

added def fin_fin.rel_embedding

added theorem injective_of_increasing

added theorem preimage_equivalence

added def rel_embedding.cod_restrict

added theorem rel_embedding.cod_restrict_apply

added theorem rel_embedding.coe_fn_inj

added theorem rel_embedding.coe_fn_mk

added theorem rel_embedding.coe_fn_to_embedding

added theorem rel_embedding.eq_preimage

added theorem rel_embedding.injective

added theorem rel_embedding.le_map_sup

added def rel_embedding.lt_embedding_of_le_embedding

added theorem rel_embedding.map_inf_le

added theorem rel_embedding.map_rel_iff

added def rel_embedding.of_monotone

added theorem rel_embedding.of_monotone_coe

added def rel_embedding.preimage

added theorem rel_embedding.refl_apply

added def rel_embedding.rsymm

added theorem rel_embedding.trans_apply

added structure rel_embedding

added theorem rel_iso.apply_inv_self

added theorem rel_iso.apply_symm_apply

added theorem rel_iso.coe_coe_fn

added theorem rel_iso.coe_fn_injective

added theorem rel_iso.coe_fn_mk

added theorem rel_iso.coe_fn_symm_mk

added theorem rel_iso.coe_fn_to_equiv

added theorem rel_iso.coe_mul

added theorem rel_iso.coe_one

added theorem rel_iso.ext

added theorem rel_iso.inv_apply_self

added theorem rel_iso.map_bot

added theorem rel_iso.map_inf

added theorem rel_iso.map_rel_iff''

added theorem rel_iso.map_rel_iff

added theorem rel_iso.map_sup

added theorem rel_iso.map_top

added theorem rel_iso.mul_apply

added theorem rel_iso.of_surjective_coe

added def rel_iso.prod_lex_congr

added theorem rel_iso.refl_apply

added theorem rel_iso.rel_symm_apply

added def rel_iso.rsymm

added def rel_iso.sum_lex_congr

added theorem rel_iso.symm_apply_apply

added theorem rel_iso.symm_apply_rel

added theorem rel_iso.to_equiv_injective

added def rel_iso.to_rel_embedding

added theorem rel_iso.to_rel_embedding_eq_coe

added theorem rel_iso.trans_apply

added structure rel_iso

added def set_coe_embedding

added theorem subrel.rel_embedding_apply

added def subrel

added theorem subrel_val

Modified src/order/semiconj_Sup.lean

Modified src/ring_theory/ideal/operations.lean

deleted def ideal.le_order_embedding_of_surjective

added def ideal.le_rel_embedding_of_surjective

deleted def ideal.lt_order_embedding_of_surjective

added def ideal.lt_rel_embedding_of_surjective

deleted def ideal.order_iso_of_bijective

deleted def ideal.order_iso_of_surjective

added def ideal.rel_iso_of_bijective

added def ideal.rel_iso_of_surjective

Modified src/ring_theory/localization.lean

deleted def localization_map.le_order_embedding

added def localization_map.le_rel_embedding

Modified src/ring_theory/noetherian.lean

Modified src/set_theory/cardinal_ordinal.lean

deleted def cardinal.aleph'.order_iso

deleted theorem cardinal.aleph'.order_iso_coe

added def cardinal.aleph'.rel_iso

added theorem cardinal.aleph'.rel_iso_coe

modified def cardinal.aleph'

deleted def cardinal.aleph_idx.order_iso

deleted theorem cardinal.aleph_idx.order_iso_coe

added def cardinal.aleph_idx.rel_iso

added theorem cardinal.aleph_idx.rel_iso_coe

Modified src/set_theory/cofinality.lean

deleted theorem order_iso.cof.aux

deleted theorem order_iso.cof

modified theorem ordinal.cof_cof

added theorem rel_iso.cof.aux

added theorem rel_iso.cof

Modified src/set_theory/ordinal.lean

deleted def cardinal.ord.order_embedding

deleted theorem cardinal.ord.order_embedding_coe

added def cardinal.ord.rel_embedding

added theorem cardinal.ord.rel_embedding_coe

modified def initial_seg.antisymm

modified theorem initial_seg.coe_coe_fn

modified theorem initial_seg.coe_fn_mk

deleted theorem initial_seg.coe_fn_to_order_embedding

added theorem initial_seg.coe_fn_to_rel_embedding

modified def initial_seg.of_iso

modified structure initial_seg

deleted def order_embedding.collapse

deleted theorem order_embedding.collapse_F.lt

deleted theorem order_embedding.collapse_F.not_lt

deleted def order_embedding.collapse_F

deleted theorem order_embedding.collapse_apply

deleted theorem ordinal.order_iso_enum'

deleted theorem ordinal.order_iso_enum

deleted def ordinal.order_iso_out

added theorem ordinal.rel_iso_enum'

added theorem ordinal.rel_iso_enum

added def ordinal.rel_iso_out

modified def ordinal.typein_iso

modified theorem principal_seg.coe_coe_fn

modified theorem principal_seg.coe_fn_mk

deleted theorem principal_seg.coe_fn_to_order_embedding

added theorem principal_seg.coe_fn_to_rel_embedding

modified def principal_seg.equiv_lt

modified theorem principal_seg.equiv_lt_apply

modified theorem principal_seg.equiv_lt_top

modified structure principal_seg

added def rel_embedding.collapse

added theorem rel_embedding.collapse_F.lt

added theorem rel_embedding.collapse_F.not_lt

added def rel_embedding.collapse_F

added theorem rel_embedding.collapse_apply

Modified src/set_theory/ordinal_arithmetic.lean