OAI/RepresentationTheory/RestrictedTilting/JetTriviality.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiberFunctorProof.map_binarySum line 11
2. lemma OAI.FiberFunctorProof.jetRelation_map_le line 15
3. def OAI.FiberFunctorProof.jetMap line 21
4. lemma OAI.FiberFunctorProof.jetMap_mk line 25
5. lemma OAI.FiberFunctorProof.jetMap_surjective line 30
6. lemma OAI.FiberFunctorProof.jetMap_injective line 57
7. theorem OAI.FiberFunctorProof.jetMap_bijective line 83