Documentation

HepLean.Tensors.IndexNotation.IndexList.Subperm

Subperm for index lists. #

source
def IndexNotation.IndexList.Subperm {X : Type} (l : IndexNotation.IndexList X) (l2 : IndexNotation.IndexList X) :
Prop

An IndexList l is a subpermutation of l2 if there are no duals in l, and every element of l has a unique dual in l2.

Equations
  • l.Subperm l2 = (l.withUniqueDualInOther l2 = Finset.univ)
Instances For
    source
    theorem IndexNotation.IndexList.Subperm.iff_countId_fin {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} :
    l.Subperm l2 ↔ ∀ (i : Fin l.val.length), l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1
    source
    theorem IndexNotation.IndexList.Subperm.iff_countId {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} :
    l.Subperm l2 ↔ ∀ (I : IndexNotation.Index X), l.countId I ≤ 1 ∧ (l.countId I = 1 → l2.countId I = 1)
    source
    theorem IndexNotation.IndexList.Subperm.trans {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} {l3 : IndexNotation.IndexList X} (h1 : l.Subperm l2) (h2 : l2.Subperm l3) :
    l.Subperm l3
    source
    theorem IndexNotation.IndexList.Subperm.fst_eq_contrIndexList {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.Subperm l2) :
    l.contrIndexList = l
    source
    theorem IndexNotation.IndexList.Subperm.symm {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.Subperm l2) (hl : l.length = l2.length) :
    l2.Subperm l
    source
    theorem IndexNotation.IndexList.Subperm.contr_refl {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} :
    l.contrIndexList.Subperm l.contrIndexList