OAI/Algebra/Finitistic/Selected/SelectedFixedDiagram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.encoding line 10
  2. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.P line 11
  3. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.theta line 12
  4. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.e line 13
  5. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.alpha line 14
  6. lemma OAI.LittleFinitistic.SelectedFixedDiagram.idem line 15
  7. lemma OAI.LittleFinitistic.SelectedFixedDiagram.central line 16
  8. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.U line 23
  9. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.oddDouble line 24
  10. abbrev OAI.LittleFinitistic.SelectedFixedDiagram.selectedAction line 25
  11. structure OAI.LittleFinitistic.SelectedFixedDiagram.Data line 29

    Source documentation

    All choices, arrows, relation-basis equations and equivariant identifications for the actual selecting algebra. No evaluation module is a parameter.

    structure Data where
…
  12. def OAI.LittleFinitistic.SelectedFixedDiagram.fixed line 51

    Source documentation

    Choose once, using the proved native finite-diagram theorem and actual theta.

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

    Mentions: OAI.LittleFinitistic.SelectedFixedDiagram.Data

  13. theorem OAI.LittleFinitistic.SelectedFixedDiagram.fixed_relations line 56
  14. theorem OAI.LittleFinitistic.SelectedFixedDiagram.fixed_equivariant line 59