← Mathematical handbook

noncomputable def Verification.finiteRanks {n : ℕ} {α : Type u_1} [LinearOrder α] (x : Fin n → α) (hx : Function.Injective x) : Equiv.Perm (Fin n)

Sort distinct observations into a rank permutation.

Equations

• Verification.finiteRanks x hx = (Equiv.ofInjective x hx).trans (Fintype.orderIsoFinOfCardEq ↑(Set.range x) ⋯).symm.toEquiv

theorem Verification.finiteRanks_le_iff {n : ℕ} {α : Type u_1} [LinearOrder α] (x : Fin n → α) (hx : Function.Injective x) (i j : Fin n) : (finiteRanks x hx) i ≤ (finiteRanks x hx) j ↔ x i ≤ x j

theorem Verification.rankPermutation_unique {n : ℕ} (r s : Equiv.Perm (Fin n)) (h : ∀ (i j : Fin n), r i ≤ r j ↔ s i ≤ s j) : r = s

theorem Verification.finiteRanks_comp_mono {n : ℕ} {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (x : Fin n → α) (f : α → β) (hf : Monotone f) (hx : Function.Injective x) (hfx : Function.Injective fun (i : Fin n) => f (x i)) : finiteRanks x hx = finiteRanks (fun (i : Fin n) => f (x i)) hfx