source
structure Vector.Perm {α : Type u_1} {n : Nat} (as bs : Vector α n) :
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_toArray_perm :: (

- toArray : as.toArray.Perm bs.toArray

- )

Instances For

source
def Vector.«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

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

Instances For

source
theorem Vector.perm_iff_toArray_perm {α : Type u_1} {n : Nat} {as bs : Vector α n} :
as.Perm bs ↔ as.toArray.Perm bs.toArray
source
theorem Vector.perm_iff_toList_perm {α : Type u_1} {n : Nat} {as bs : Vector α n} :
as.Perm bs ↔ as.toList.Perm bs.toList
source
theorem Vector.Perm.of_toList_perm {α : Type u_1} {n : Nat} {as bs : Vector α n} :
as.toList.Perm bs.toList → as.Perm bs
source
theorem Vector.Perm.toList {α : Type u_1} {n : Nat} {as bs : Vector α n} :
as.Perm bs → as.toList.Perm bs.toList
source
@[simp]
theorem Vector.perm_mk {α : Type u_1} {n : Nat} (as bs : Array α) (ha : as.size = n) (hb : bs.size = n) :
(mk as ha).Perm (mk bs hb) ↔ as.Perm bs
source
theorem Vector.toArray_perm_iff {α : Type u_1} {n : Nat} (xs : Vector α n) (ys : Array α) :
xs.toArray.Perm ys ↔ ∃ (h : ys.size = n), xs.Perm (mk ys h)
source
theorem Vector.perm_toArray_iff {α : Type u_1} {n : Nat} (xs : Array α) (ys : Vector α n) :
xs.Perm ys.toArray ↔ ∃ (h : xs.size = n), (mk xs h).Perm ys
source
@[simp]
theorem Vector.Perm.refl {α : Type u_1} {n : Nat} (xs : Vector α n) :
xs.Perm xs
source
theorem Vector.Perm.rfl {α : Type u_1} {n : Nat} {xs : Vector α n} :
xs.Perm xs
source
theorem Vector.Perm.of_eq {α : Type u_1} {n : Nat} {xs ys : Vector α n} (h : xs = ys) :
xs.Perm ys
source
theorem Vector.Perm.symm {α : Type u_1} {n : Nat} {xs ys : Vector α n} (h : xs.Perm ys) :
ys.Perm xs
source
theorem Vector.Perm.trans {α : Type u_1} {n : Nat} {xs ys zs : Vector α n} (h₁ : xs.Perm ys) (h₂ : ys.Perm zs) :
xs.Perm zs
source
instance Vector.instTransPerm {α : Type u_1} {n : Nat} :
Trans Perm Perm Perm
Equations

- Vector.instTransPerm = { trans := ⋯ }

source
theorem Vector.perm_comm {α : Type u_1} {n : Nat} {xs ys : Vector α n} :
xs.Perm ys ↔ ys.Perm xs
source
theorem Vector.Perm.mem_iff {α : Type u_1} {n : Nat} {a : α} {xs ys : Vector α n} (p : xs.Perm ys) :
a ∈ xs ↔ a ∈ ys
source
theorem Vector.Perm.append {α : Type u_1} {m n : Nat} {xs ys : Vector α m} {as bs : Vector α n} (p₁ : xs.Perm ys) (p₂ : as.Perm bs) :
(xs ++ as).Perm (ys ++ bs)
source
theorem Vector.Perm.push {α : Type u_1} {n : Nat} (x : α) {xs ys : Vector α n} (p : xs.Perm ys) :
(xs.push x).Perm (ys.push x)
source
theorem Vector.Perm.push_comm {α : Type u_1} {n : Nat} (x y : α) {xs ys : Vector α n} (p : xs.Perm ys) :
((xs.push x).push y).Perm ((ys.push y).push x)
source
theorem Vector.swap_perm {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (h₁ : i < n) (h₂ : j < n) :
(xs.swap i j h₁ h₂).Perm xs
source
theorem Vector.Perm.extract {α : Type u_1} {n : Nat} {xs ys : Vector α n} (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)