TupleSplitting.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Splitting distinct ordered words at a cut

Concatenation identifies injective ordered words with pairs of injective subwords having disjoint underlying subsets. At a preservation cut the unique omitted label is recovered from the complementary singleton.

abbrev OAI.KadisonKastler.DisjointOrderedTuplePair line 24
def OAI.KadisonKastler.tupleInitial line 28
def OAI.KadisonKastler.tupleFinal line 34
theorem OAI.KadisonKastler.tupleInitial_final_disjoint line 41
def OAI.KadisonKastler.tupleSplit line 53
def OAI.KadisonKastler.tupleJoin line 57
theorem OAI.KadisonKastler.tupleInitial_join line 72
theorem OAI.KadisonKastler.tupleFinal_join line 80
theorem OAI.KadisonKastler.tupleJoin_split line 88
def OAI.KadisonKastler.orderedTupleSplitEquiv line 94
Source documentation
The exact word-to-pair bijection at a cut without preservation.
```
def orderedTupleSplitEquiv (W : Finset α) (p q : ℕ) :
    OrderedLabelTuple W (p + q) ≃ DisjointOrderedTuplePair W p q where
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.DisjointOrderedTuplePair
theorem OAI.KadisonKastler.orderedTupleList_join line 105
theorem OAI.KadisonKastler.tupleSubset_join line 112
theorem OAI.KadisonKastler.tupleSubset_initial_subset line 120
theorem OAI.KadisonKastler.tupleSubset_final_subset line 130
theorem OAI.KadisonKastler.sum_orderedTuple_split line 139
theorem OAI.KadisonKastler.sum_disjointOrderedTuplePair line 144
def OAI.KadisonKastler.tupleSingleton line 153
theorem OAI.KadisonKastler.tupleSubset_singleton line 158
theorem OAI.KadisonKastler.orderedTupleList_singleton line 165
def OAI.KadisonKastler.tuplePairMissing line 169
theorem OAI.KadisonKastler.tuplePairMissing_spec line 174
theorem OAI.KadisonKastler.tuplePairMissing_mem_sdiff line 182
theorem OAI.KadisonKastler.tuplePairMissing_mem line 189
theorem OAI.KadisonKastler.tuplePairMissing_not_initial line 194
theorem OAI.KadisonKastler.tuplePairMissing_not_final line 201
def OAI.KadisonKastler.tupleMissingPrefix line 207
def OAI.KadisonKastler.tupleMissingJoinPair line 213
def OAI.KadisonKastler.tupleInsertMiddle line 223
Source documentation
Insert the missing label between the two subwords.
```
def tupleInsertMiddle {W : Finset α} {p q : ℕ} (hW : W.card = p + 1 + q)
    (ab : DisjointOrderedTuplePair W p q) : OrderedLabelTuple W (p + 1 + q) :=
…
```
Mentions: OAI.KadisonKastler.DisjointOrderedTuplePair, OAI.KadisonKastler.OrderedLabelTuple
def OAI.KadisonKastler.tupleDropMiddle line 228
Source documentation
Drop the distinguished middle position of a word.
```
def tupleDropMiddle {W : Finset α} {p q : ℕ}
    (t : OrderedLabelTuple W (p + 1 + q)) : DisjointOrderedTuplePair W p q :=
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.DisjointOrderedTuplePair
def OAI.KadisonKastler.tupleMiddle line 233
theorem OAI.KadisonKastler.tupleMiddle_mem_sdiff line 237
theorem OAI.KadisonKastler.tuplePairMissing_dropMiddle line 252
theorem OAI.KadisonKastler.tupleDropMiddle_insertMiddle line 261
theorem OAI.KadisonKastler.tupleInsertMiddle_dropMiddle line 274
def OAI.KadisonKastler.orderedTupleMiddleEquiv line 296
Source documentation
The preservation-cut bijection recovers the omitted middle letter from the complementary singleton of the two retained subwords.
```
def orderedTupleMiddleEquiv (W : Finset α) (p q : ℕ) (hW : W.card = p + 1 + q) :
    OrderedLabelTuple W (p + 1 + q) ≃ DisjointOrderedTuplePair W p q where
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.DisjointOrderedTuplePair
theorem OAI.KadisonKastler.tupleMiddle_insertMiddle line 305
theorem OAI.KadisonKastler.orderedTupleList_insertMiddle line 313
theorem OAI.KadisonKastler.sum_orderedTuple_middle line 324