OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorDirected.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.bIndex line 12
2. def OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.cIndex line 13
3. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.index_value line 15
4. def OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.vertex line 18
5. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.vertex_idempotent line 20
6. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.vertex_orthogonal line 23
7. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.vertex_complete line 37
8. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.vertex_diagonal line 47
9. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.vertex_directed line 61
10. def OAI.LittleFinitistic.OrdinarySimulation.TensorDirected.directedSystem line 83

    Source documentation

    A concrete linear extension of the source's product order, with exactly 3n vertices.

    def directedSystem : DirectedBound.DirectedSystem k (B ⊗[k] C) (n*3) where
    …

    Mentions: OAI.LittleFinitistic.DirectedBound.DirectedSystem