EqualityPatterns.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A finite set-partition expansion, presented by explicit surjective block labels. This separates the finite combinatorics from complex matrix moments.

structure OAI.MUB6.EqualityPatterns.Family line 19
Source documentation
Each label p is a surjection onto the blocks of one partition.
```
structure Family (A P : Type*) where
…
```
def OAI.MUB6.EqualityPatterns.Family.flatten line 27
theorem OAI.MUB6.EqualityPatterns.Family.flatten_injective line 30
theorem OAI.MUB6.EqualityPatterns.Family.flatten_surjective line 51
def OAI.MUB6.EqualityPatterns.Family.assignmentsEquiv line 71
Source documentation
Every function has exactly one equality pattern and an injection assigning distinct values to its blocks. No probabilistic premise is used.
```
def assignmentsEquiv (F : Family A P)
    (cover : ∀ f : A → B, ∃ p, ∀ i j,
      F.label p i = F.label p j ↔ f i = f j) :
    (Σ p, Fin (F.blocks p) ↪ B) ≃ (A → B) :=
…
```
Mentions: OAI.MUB6.EqualityPatterns.Family
theorem OAI.MUB6.EqualityPatterns.Family.sum_assignments line 77