Sort

📁 Source: Mathlib/Data/Fin/Tuple/Sort.lean

Statistics

Metric	Count
Definitions graph, proj, graphEquiv₁, graphEquiv₂, sort	5
Theorems monotone_iff, antitone_pair_of_not_sorted, antitone_pair_of_not_sorted', comp_perm_comp_sort_eq_comp_sort, comp_sort_eq_comp_iff_monotone, eq_sort_iff, eq_sort_iff', card, graphEquiv₂_apply, lt_card_ge_iff_apply_ge_of_antitone, lt_card_gt_iff_apply_gt_of_antitone, lt_card_le_iff_apply_le_of_monotone, lt_card_lt_iff_apply_lt_of_monotone, monotone_proj, monotone_sort, proj_equiv₁', self_comp_sort, sort_eq_refl_iff_monotone, sort_perm, unique_antitone, unique_monotone	21
Total	26

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monotone_iff 📖	mathematical	—	Monotone PartialOrder.toPreorder Fin.instPartialOrder DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instOne	—	Tuple.sort_eq_refl_iff_monotone Tuple.sort_perm inv_eq_one one_def

Tuple

Definitions

Name	Category	Theorems
graph 📖	CompOp	6 math math: monotone_proj, graphEquiv₂_apply, self_comp_sort, graph.card, eq_sort_iff', proj_equiv₁'
graphEquiv₁ 📖	CompOp	3 math math: graphEquiv₂_apply, eq_sort_iff', proj_equiv₁'
graphEquiv₂ 📖	CompOp	2 math math: graphEquiv₂_apply, self_comp_sort
sort 📖	CompOp	13 math math: sort_perm, sort_eq_refl_iff_monotone, graphEquiv₂_apply, self_comp_sort, bubble_sort_induction', comp_sort_eq_comp_iff_monotone, eq_sort_iff, LinearMap.IsSymmetric.eigenvalues_def, eq_sort_iff', comp_perm_comp_sort_eq_comp_sort, bubble_sort_induction, monotone_sort, LinearMap.IsSymmetric.eigenvectorBasis_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_pair_of_not_sorted 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	antitone_pair_of_not_sorted'
antitone_pair_of_not_sorted' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq comp_sort_eq_comp_iff_monotone monotone_iff_forall_lt
comp_perm_comp_sort_eq_comp_sort 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike sort	—	Function.comp_assoc Equiv.Perm.coe_mul unique_monotone monotone_sort
comp_sort_eq_comp_iff_monotone 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike sort Monotone PartialOrder.toPreorder Fin.instPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	monotone_sort unique_monotone
eq_sort_iff 📖	mathematical	—	sort Monotone PartialOrder.toPreorder Fin.instPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	eq_sort_iff' Monotone.comp monotone_proj StrictMono.monotone Prod.Lex.toLex_lt_toLex Eq.not_lt LE.le.eq_or_lt LT.lt.le
eq_sort_iff' 📖	mathematical	—	sort StrictMono Lex Finset SetLike.instMembership Finset.instSetLike graph PartialOrder.toPreorder Fin.instPartialOrder Subtype.preorder Prod.Lex.instPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.trans graphEquiv₁	—	sort.eq_1 Equiv.trans_assoc Equiv.symm_trans_self OrderIso.strictMono Equiv.surjective OrderIso.subsingleton_of_wellFoundedGT' IsWellOrder.toIsWellFounded isWellOrder_gt Finite.to_wellFoundedGT Finite.of_fintype Equiv.Perm.ext Equiv.apply_eq_iff_eq_symm_apply DFunLike.congr_fun
graphEquiv₂_apply 📖	mathematical	—	DFunLike.coe OrderIso Lex Finset SetLike.instMembership Finset.instSetLike graph Prod.Lex.instLE Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderIso graphEquiv₂ Equiv EquivLike.toFunLike Equiv.instEquivLike graphEquiv₁ Equiv.Perm sort	—	Equiv.apply_symm_apply
lt_card_ge_iff_apply_ge_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder Fin.instPartialOrder	Finset.card Finset.filter Preorder.toLE Finset.univ Fin.fintype	—	Fin.lt_card_filter_univ_iff_apply_of_imp
lt_card_gt_iff_apply_gt_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder Fin.instPartialOrder	Finset.card Finset.filter Preorder.toLT Finset.univ Fin.fintype	—	Fin.lt_card_filter_univ_iff_apply_of_imp
lt_card_le_iff_apply_le_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder Fin.instPartialOrder	Finset.card Finset.filter Preorder.toLE Finset.univ Fin.fintype	—	Fin.lt_card_filter_univ_iff_apply_of_imp
lt_card_lt_iff_apply_lt_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder Fin.instPartialOrder	Finset.card Finset.filter Preorder.toLT Finset.univ Fin.fintype	—	Fin.lt_card_filter_univ_iff_apply_of_imp
monotone_proj 📖	mathematical	—	Monotone Lex Finset SetLike.instMembership Finset.instSetLike graph Subtype.preorder Prod.Lex.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Fin.instPartialOrder graph.proj	—	le_of_lt
monotone_sort 📖	mathematical	—	Monotone PartialOrder.toPreorder Fin.instPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike sort	—	self_comp_sort Monotone.comp monotone_proj OrderIso.monotone
proj_equiv₁' 📖	mathematical	—	Lex Finset SetLike.instMembership Finset.instSetLike graph graph.proj DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike graphEquiv₁	—	—
self_comp_sort 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike sort Lex Finset SetLike.instMembership Finset.instSetLike graph graph.proj OrderIso Prod.Lex.instLE Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderIso graphEquiv₂	—	Equiv.self_comp_symm
sort_eq_refl_iff_monotone 📖	mathematical	—	sort Equiv.refl Monotone PartialOrder.toPreorder Fin.instPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eq_sort_iff Equiv.coe_refl
sort_perm 📖	mathematical	—	sort Fin.instLinearOrder DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instInv	—	eq_sort_iff Equiv.self_comp_symm monotone_id LT.lt.ne Equiv.apply_symm_apply
unique_antitone 📖	—	Antitone PartialOrder.toPreorder Fin.instPartialOrder DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	—	List.ofFn_injective List.Perm.eq_of_pairwise' instAntisymmGe List.SortedGE.pairwise Antitone.sortedGE_ofFn Equiv.Perm.ofFn_comp_perm
unique_monotone 📖	—	Monotone PartialOrder.toPreorder Fin.instPartialOrder DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	—	List.ofFn_injective List.Perm.eq_of_pairwise' instAntisymmLe List.SortedLE.pairwise Monotone.sortedLE_ofFn Equiv.Perm.ofFn_comp_perm

Tuple.graph

Definitions

Name	Category	Theorems
proj 📖	CompOp	3 math math: Tuple.monotone_proj, Tuple.self_comp_sort, Tuple.proj_equiv₁'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Lex Tuple.graph	—	eq_1 Finset.card_image_of_injective Finset.card_fin

---

← Back to Index