OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalBinary.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.IntervalBar.Diagram.oneEvalline 11 - def
OAI.IntervalBar.Diagram.oneConstline 12 - def
OAI.IntervalBar.Diagram.piOneEquivline 13 - instance
OAI.IntervalBar.Diagram.oneEval_equivalenceline 29 - def
OAI.IntervalBar.Diagram.tensorPairline 33 - def
OAI.IntervalBar.Diagram.binaryCutline 38 - lemma
OAI.IntervalBar.Diagram.binary_zeroline 42 - lemma
OAI.IntervalBar.Diagram.binary_lastline 44 - def
OAI.IntervalBar.Diagram.binaryFaceline 46 - def
OAI.IntervalBar.Diagram.binaryFaceZeroline 48 - def
OAI.IntervalBar.Diagram.binaryFaceLastline 52 - def
OAI.IntervalBar.Diagram.binaryCutIsoline 56 - def
OAI.IntervalBar.Diagram.binaryFaceMiddleline 60