OAI/Algebra/Finitistic/Selected/SelectedChainDiagram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedChainDiagram.D0 line 10
2. abbrev OAI.LittleFinitistic.SelectedChainDiagram.D1 line 11
3. abbrev OAI.LittleFinitistic.SelectedChainDiagram.D2 line 12
4. structure OAI.LittleFinitistic.SelectedChainDiagram.Data line 15

   Source documentation

   Chain representatives and all specified relation homotopies for the one fixed diagram.

   structure Data where
   …

5. def OAI.LittleFinitistic.SelectedChainDiagram.fixedChain line 24

   Source documentation

   These choices, too, are made once before any evaluation module Y.

   def fixedChain : Data := Classical.choice (by
   …

   Mentions: OAI.LittleFinitistic.SelectedChainDiagram.Data

6. theorem OAI.LittleFinitistic.SelectedChainDiagram.bounded line 29
7. def OAI.LittleFinitistic.SelectedChainDiagram.fK line 34
8. def OAI.LittleFinitistic.SelectedChainDiagram.gK line 36
9. theorem OAI.LittleFinitistic.SelectedChainDiagram.fK_eq line 39
10. theorem OAI.LittleFinitistic.SelectedChainDiagram.gK_eq line 43
11. theorem OAI.LittleFinitistic.SelectedChainDiagram.evaluated_f line 51
12. theorem OAI.LittleFinitistic.SelectedChainDiagram.evaluated_g line 59