structure Array.Perm {α : Type u_1} (as bs : Array α) : Prop

Perm as bs asserts that as and bs are permutations of each other.

This is a wrapper around List.Perm, and for now has much less API. For more complicated verification, use perm_iff_toList_perm and the List API.

• of_toList_perm :: (
• toList : as.toList.Perm bs.toList
• )

def Array.«term_~_» : Lean.TrailingParserDescr

Perm as bs asserts that as and bs are permutations of each other.

This is a wrapper around List.Perm, and for now has much less API. For more complicated verification, use perm_iff_toList_perm and the List API.

Equations

• Array.«term_~_» = Lean.ParserDescr.trailingNode `Array.«term_~_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

theorem Array.perm_iff_toList_perm {α : Type u_1} {as bs : Array α} : as.Perm bs ↔ as.toList.Perm bs.toList

theorem List.perm_iff_toArray_perm {α : Type u_1} {as bs : List α} : as.Perm bs ↔ as.toArray.Perm bs.toArray

theorem List.Perm.of_toArray_perm {α : Type u_1} {as bs : List α} : as.toArray.Perm bs.toArray → as.Perm bs

theorem List.Perm.toArray {α : Type u_1} {as bs : List α} : as.Perm bs → as.toArray.Perm bs.toArray

@[simp]

theorem Array.Perm.refl {α : Type u_1} (xs : Array α) : xs.Perm xs

theorem Array.Perm.rfl {α : Type u_1} {xs : Array α} : xs.Perm xs

theorem Array.Perm.of_eq {α : Type u_1} {xs ys : Array α} (h : xs = ys) : xs.Perm ys

theorem Array.Perm.symm {α : Type u_1} {xs ys : Array α} (h : xs.Perm ys) : ys.Perm xs

theorem Array.Perm.trans {α : Type u_1} {xs ys zs : Array α} (h₁ : xs.Perm ys) (h₂ : ys.Perm zs) : xs.Perm zs

instance Array.instTransPerm {α : Type u_1} : Trans Perm Perm Perm

Equations

• Array.instTransPerm = { trans := ⋯ }

theorem Array.perm_comm {α : Type u_1} {xs ys : Array α} : xs.Perm ys ↔ ys.Perm xs

theorem Array.Perm.size_eq {α : Type u_1} {xs ys : Array α} (p : xs.Perm ys) : xs.size = ys.size

@[reducible, inline, deprecated Array.Perm.size_eq (since := "2025-04-17")]

abbrev Array.Perm.length_eq {α : Type u_1} {xs ys : Array α} (p : xs.Perm ys) : xs.size = ys.size

Equations

• @Array.Perm.length_eq = @Array.Perm.size_eq

theorem Array.Perm.mem_iff {α : Type u_1} {a : α} {xs ys : Array α} (p : xs.Perm ys) : a ∈ xs ↔ a ∈ ys

theorem Array.Perm.append {α : Type u_1} {xs ys as bs : Array α} (p₁ : xs.Perm ys) (p₂ : as.Perm bs) : (xs ++ as).Perm (ys ++ bs)

theorem Array.Perm.push {α : Type u_1} (x : α) {xs ys : Array α} (p : xs.Perm ys) : (xs.push x).Perm (ys.push x)

theorem Array.Perm.push_comm {α : Type u_1} (x y : α) {xs ys : Array α} (p : xs.Perm ys) : ((xs.push x).push y).Perm ((ys.push y).push x)

theorem Array.swap_perm {α : Type u_1} {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < xs.size) : (xs.swap i j h₁ h₂).Perm xs

theorem Array.Perm.extract {α : Type u_1} {xs ys : Array α} (h : xs.Perm ys) {lo hi : Nat} (wlo : ∀ (i : Nat), i < lo → xs[i]? = ys[i]?) (whi : ∀ (i : Nat), hi ≤ i → xs[i]? = ys[i]?) : (xs.extract lo hi).Perm (ys.extract lo hi)