Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-03 02:24 9f252442

View on Github →

chore(data/finset/sort): upgrade finset.mono_of_fin to an order_iso (#5495)

Upgrade finset.mono_of_fin to an order_embedding.
Drop some lemmas that now immediately follow from order_embedding.*.
Upgrade finset.mono_equiv_of_fin to order_iso.
Define list.nodup.nth_le_equiv and list.sorted.nth_le_iso.
Upgrade mono_equiv_of_fin to an order_iso, make it computable.

Estimated changes

Modified src/analysis/normed_space/multilinear.lean

Modified src/combinatorics/composition.lean

deleted theorem composition.mono_of_fin_boundaries

added theorem composition.order_emb_of_fin_boundaries

modified def composition_as_set.boundary

modified theorem composition_as_set.boundary_zero

Modified src/data/finset/basic.lean

added theorem finset.coe_fin_range

Modified src/data/finset/sort.lean

added theorem finset.coe_order_iso_of_fin_apply

deleted def finset.mono_of_fin

deleted theorem finset.mono_of_fin_bij_on

deleted theorem finset.mono_of_fin_eq_mono_of_fin_iff

deleted theorem finset.mono_of_fin_injective

deleted theorem finset.mono_of_fin_last

deleted theorem finset.mono_of_fin_singleton

deleted theorem finset.mono_of_fin_strict_mono

deleted theorem finset.mono_of_fin_unique'

deleted theorem finset.mono_of_fin_unique

deleted theorem finset.mono_of_fin_zero

added def finset.order_emb_of_fin

added theorem finset.order_emb_of_fin_apply

added theorem finset.order_emb_of_fin_eq_order_emb_of_fin_iff

added theorem finset.order_emb_of_fin_last

added theorem finset.order_emb_of_fin_singleton

added theorem finset.order_emb_of_fin_unique'

added theorem finset.order_emb_of_fin_unique

added theorem finset.order_emb_of_fin_zero

added def finset.order_iso_of_fin

added theorem finset.order_iso_of_fin_symm_apply

deleted theorem finset.range_mono_of_fin

added theorem finset.range_order_emb_of_fin

modified theorem finset.sort_sorted_lt

Modified src/data/fintype/sort.lean

added def mono_equiv_of_fin

Created src/data/list/nodup_equiv_fin.lean

added theorem list.nodup.coe_nth_le_equiv_apply

added theorem list.nodup.coe_nth_le_equiv_symm_apply

added def list.nodup.nth_le_equiv

added theorem list.sorted.coe_nth_le_iso_apply

added theorem list.sorted.coe_nth_le_iso_symm_apply

added def list.sorted.nth_le_iso

added theorem list.sorted.nth_le_mono

added theorem list.sorted.nth_le_strict_mono

Modified src/linear_algebra/affine_space/independent.lean

added theorem affine.simplex.face_points'

Modified src/linear_algebra/multilinear.lean

added def multilinear_map.restr