OAI/Analysis/Cotype/FrameLifts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Cotype.primalTupleAction line 11
2. def OAI.Cotype.dualTupleAction line 16
3. theorem OAI.Cotype.exists_primal_tuple_lifts line 24
4. theorem OAI.Cotype.exists_dual_tuple_lifts line 37
5. abbrev OAI.Cotype.GrowthSpace line 51
6. structure OAI.Cotype.GrowthPairingData line 53
7. theorem OAI.Cotype.exists_growthPairingData line 76