OrderedTuples.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Ordering fibres of distinct label tuples

An injective ordered tuple determines its underlying subset. Every fibre consists of the bijections from the positions onto that subset, so its cardinality is exactly the factorial of the number of positions.

def OAI.KadisonKastler.OrderedLabelTuple line 23
instance OAI.KadisonKastler.(instance at line 26) line 26
def OAI.KadisonKastler.tupleSubset line 32
Source documentation
Forget the ordering of the distinct labels.
```
def tupleSubset {W : Finset α} {p : ℕ} (t : OrderedLabelTuple W p) : WordSubset W p :=
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.WordSubset
theorem OAI.KadisonKastler.mem_tupleSubset line 44
def OAI.KadisonKastler.orderedTupleOfEquiv line 49
Source documentation
Realize a bijective enumeration of a subset as an ordered tuple in W.
```
def orderedTupleOfEquiv {W : Finset α} {p : ℕ} (B : WordSubset W p)
    (e : Fin p ≃ B.val) : OrderedLabelTuple W p :=
…
```
Mentions: OAI.KadisonKastler.WordSubset, OAI.KadisonKastler.OrderedLabelTuple
theorem OAI.KadisonKastler.tupleSubset_orderedTupleOfEquiv line 59
def OAI.KadisonKastler.orderedTupleEquiv line 72
Source documentation
Enumerate the subset from an ordered tuple known to lie over it.
```
def orderedTupleEquiv {W : Finset α} {p : ℕ} (B : WordSubset W p)
    (t : OrderedLabelTuple W p) (ht : tupleSubset t = B) : Fin p ≃ B.val :=
…
```
Mentions: OAI.KadisonKastler.WordSubset, OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.tupleSubset
def OAI.KadisonKastler.orderedTupleFiberEquiv line 89
Source documentation
An ordering fibre is the type of bijections from its positions onto its underlying subset.
```
def orderedTupleFiberEquiv {W : Finset α} {p : ℕ} (B : WordSubset W p) :
    {t : OrderedLabelTuple W p // tupleSubset t = B} ≃ (Fin p ≃ B.val) where
…
```
Mentions: OAI.KadisonKastler.WordSubset, OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.tupleSubset
theorem OAI.KadisonKastler.card_orderedTupleFiber line 105
Source documentation
Every p-element subset has exactly p! orderings.
```
theorem card_orderedTupleFiber {W : Finset α} {p : ℕ} (B : WordSubset W p) :
    Fintype.card {t : OrderedLabelTuple W p // tupleSubset t = B} = p.factorial := by
…
```
Mentions: OAI.KadisonKastler.WordSubset, OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.tupleSubset
theorem OAI.KadisonKastler.card_filter_tupleSubset line 114
Source documentation
The finset form used by the matrix replication estimate.
```
theorem card_filter_tupleSubset {W : Finset α} {p : ℕ} (B : WordSubset W p) :
    #{t : OrderedLabelTuple W p | tupleSubset t = B} = p.factorial := by
…
```
Mentions: OAI.KadisonKastler.WordSubset, OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.tupleSubset
theorem OAI.KadisonKastler.card_orderedLabelTuple line 121
Source documentation
Count ordered selections by first choosing their underlying subset.
```
theorem card_orderedLabelTuple (W : Finset α) (p : ℕ) :
    Fintype.card (OrderedLabelTuple W p) = W.card.choose p * p.factorial := by
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple
theorem OAI.KadisonKastler.card_full_orderedLabelTuple line 129
Source documentation
In particular, all orderings of an r-element label set number r!.
```
theorem card_full_orderedLabelTuple (W : Finset α) {r : ℕ} (hr : W.card = r) :
    Fintype.card (OrderedLabelTuple W r) = r.factorial := by
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple
def OAI.KadisonKastler.orderedTupleList line 134
Source documentation
The ordered list used to form a noncommutative word.
```
def orderedTupleList {W : Finset α} {p : ℕ} (t : OrderedLabelTuple W p) : List α :=
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple
theorem OAI.KadisonKastler.length_orderedTupleList line 139
theorem OAI.KadisonKastler.nodup_orderedTupleList line 144
theorem OAI.KadisonKastler.toFinset_orderedTupleList line 150
theorem OAI.KadisonKastler.orderedTupleList_injective line 156