Documentation

HepLean.Tensors.IndexNotation.ColorIndexList.Append

Appending two ColorIndexLists #

We define conditional appending of ColorIndexList's.

It is conditional on AppendCond being true, which we define.

Append #

source
def IndexNotation.ColorIndexList.AppendCond {𝓒 : TensorColor} [IndexNotation 𝓒.Color] (l : IndexNotation.ColorIndexList 𝓒) (l2 : IndexNotation.ColorIndexList 𝓒) :
Prop

The condition on the ColorIndexLists l and l2 so that on appending they form a ColorIndexList.

Note: AppendCond does not form an equivalence relation as it is not reflexive or transitive.

Equations
  • l.AppendCond l2 = ((l.toIndexList ++ l2.toIndexList).OnlyUniqueDuals ∧ (l.toIndexList ++ l2.toIndexList).ColorCond)
Instances For
    source
    def IndexNotation.ColorIndexList.append {𝓒 : TensorColor} [IndexNotation 𝓒.Color] (l : IndexNotation.ColorIndexList 𝓒) (l2 : IndexNotation.ColorIndexList 𝓒) (h : l.AppendCond l2) :
    IndexNotation.ColorIndexList 𝓒

    Given two ColorIndexLists satisfying AppendCond. The correponding combined ColorIndexList.

    Equations
    • l.append l2 h = { toIndexList := l.toIndexList ++ l2.toIndexList, unique_duals := β‹―, dual_color := β‹― }
    Instances For
      source
      def IndexNotation.ColorIndexList.Β«term_++[_]_Β» :
      Lean.TrailingParserDescr

      The join of two ColorIndexList satisfying the condition AppendCond that they can be appended to form a ColorIndexList.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem IndexNotation.ColorIndexList.append_toIndexList {𝓒 : TensorColor} [IndexNotation 𝓒.Color] (l : IndexNotation.ColorIndexList 𝓒) (l2 : IndexNotation.ColorIndexList 𝓒) (h : l.AppendCond l2) :
        (l.append l2 h).toIndexList = l.toIndexList ++ l2.toIndexList
        source
        theorem IndexNotation.ColorIndexList.AppendCond.symm {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) :
        l2.AppendCond l
        source
        theorem IndexNotation.ColorIndexList.AppendCond.inr {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} {l3 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) (h' : (l.append l2 h).AppendCond l3) :
        l2.AppendCond l3
        source
        theorem IndexNotation.ColorIndexList.AppendCond.assoc {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} {l3 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) (h' : (l.append l2 h).AppendCond l3) :
        l.AppendCond (l2.append l3 β‹―)
        source
        theorem IndexNotation.ColorIndexList.AppendCond.swap {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} {l3 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) (h' : (l.append l2 h).AppendCond l3) :
        (l2.append l β‹―).AppendCond l3
        source
        theorem IndexNotation.ColorIndexList.AppendCond.contr_left {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) :
        l.contr.AppendCond l2

        If AppendCond l l2 then AppendCond l.contr l2. Note that the inverse is generally not true.

        source
        theorem IndexNotation.ColorIndexList.AppendCond.contr_right {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) :
        l.AppendCond l2.contr
        source
        theorem IndexNotation.ColorIndexList.AppendCond.contr {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) :
        l.contr.AppendCond l2.contr
        source
        def IndexNotation.ColorIndexList.AppendCond.bool {𝓒 : TensorColor} [DecidableEq 𝓒.Color] (l : IndexNotation.IndexList 𝓒.Color) (l2 : IndexNotation.IndexList 𝓒.Color) :
        Bool

        A boolean which is true for two index lists l and l2 if on appending they can form a ColorIndexList.

        Equations
        Instances For
          source
          theorem IndexNotation.ColorIndexList.AppendCond.bool_iff {𝓒 : TensorColor} [DecidableEq 𝓒.Color] (l : IndexNotation.IndexList 𝓒.Color) (l2 : IndexNotation.IndexList 𝓒.Color) :
          IndexNotation.ColorIndexList.AppendCond.bool l l2 = true ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ∧ IndexNotation.IndexList.ColorCond.bool (l ++ l2) = true
          source
          theorem IndexNotation.ColorIndexList.AppendCond.iff_bool {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] (l : IndexNotation.ColorIndexList 𝓒) (l2 : IndexNotation.ColorIndexList 𝓒) :
          l.AppendCond l2 ↔ IndexNotation.ColorIndexList.AppendCond.bool l.toIndexList l2.toIndexList = true
          source
          theorem IndexNotation.ColorIndexList.AppendCond.countId_contr_fst_eq_zero_mem_snd {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) {I : IndexNotation.Index 𝓒.Color} (hI : I ∈ l2.val) :
          l.contr.countId I = 0 ↔ l.countId I = 0
          source
          theorem IndexNotation.ColorIndexList.AppendCond.countId_contr_snd_eq_zero_mem_fst {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] {l : IndexNotation.ColorIndexList 𝓒} {l2 : IndexNotation.ColorIndexList 𝓒} (h : l.AppendCond l2) {I : IndexNotation.Index 𝓒.Color} (hI : I ∈ l.val) :
          l2.contr.countId I = 0 ↔ l2.countId I = 0
          source
          theorem IndexNotation.ColorIndexList.append_contr_left {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] (l : IndexNotation.ColorIndexList 𝓒) (l2 : IndexNotation.ColorIndexList 𝓒) (h : l.AppendCond l2) :
          (l.contr.append l2 β‹―).contr = (l.append l2 h).contr
          source
          theorem IndexNotation.ColorIndexList.append_contr_right {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] (l : IndexNotation.ColorIndexList 𝓒) (l2 : IndexNotation.ColorIndexList 𝓒) (h : l.AppendCond l2) :
          (l.append l2.contr β‹―).contr = (l.append l2 h).contr
          source
          theorem IndexNotation.ColorIndexList.append_contr {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color] (l : IndexNotation.ColorIndexList 𝓒) (l2 : IndexNotation.ColorIndexList 𝓒) (h : l.AppendCond l2) :
          (l.contr.append l2.contr β‹―).contr = (l.append l2 h).contr