OAI/Analysis/WeakInfiniteness/TensorFunctoriality.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.spatialMapRight line 22
2. lemma OAI.WeakPureInfiniteness.spatialMapRight_elementary line 33
3. lemma OAI.WeakPureInfiniteness.spatialElementary_mem line 36
4. def OAI.WeakPureInfiniteness.minimalElementary line 41
5. lemma OAI.WeakPureInfiniteness.spatialMapRight_mem line 44
6. def OAI.WeakPureInfiniteness.minimalMapRight line 56
7. lemma OAI.WeakPureInfiniteness.minimalMapRight_elementary line 62
8. theorem OAI.WeakPureInfiniteness.minimalMapRight_surjective line 65