EncodingGenerators.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.EncodingGenerators.first line 12
Source documentation
The entire first arrow space inside the encoding algebra.
```
def first : Arrows k d →ₗ[k] B P where
…
```
def OAI.LittleFinitistic.EncodingGenerators.second line 18
Source documentation
The entire second arrow space inside the encoding algebra.
```
def second : Arrows k d →ₗ[k] B P where
…
```
lemma OAI.LittleFinitistic.EncodingGenerators.first_mem line 23
lemma OAI.LittleFinitistic.EncodingGenerators.second_mem line 32
lemma OAI.LittleFinitistic.EncodingGenerators.path_mem line 41
theorem OAI.LittleFinitistic.EncodingGenerators.eq_top line 60
Source documentation
Vertices and the specified finite arrow list generate the full encoding, including the quotient length-two path component.
```
theorem eq_top (S : Subalgebra k (B P))
    (hv : ∀ i, ThreeVertexAlgebra.vertex (composition P) i ∈ S)
    (h01 : ∀ a, arrow01 P a ∈ S) (h12 : ∀ a, arrow12 P a ∈ S) : S = ⊤ := by
…
```
Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra.vertex