OAI/Analysis/WeakInfiniteness/OInfinityMap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.oInfinity_graph_bound line 28
2. def OAI.WeakPureInfiniteness.oInfinityGraph line 44
3. instance OAI.WeakPureInfiniteness.oInfinityGraphCStar line 47
4. def OAI.WeakPureInfiniteness.oInfinityGraphFirst line 49
5. lemma OAI.WeakPureInfiniteness.oInfinityGraphFirst_isometry line 52
6. lemma OAI.WeakPureInfiniteness.oInfinityGraphFirst_surjective line 63
7. def OAI.WeakPureInfiniteness.oInfinityMap line 93
8. lemma OAI.WeakPureInfiniteness.oInfinityMap_isometry line 101
9. lemma OAI.WeakPureInfiniteness.oInfinity_generators_dense line 114
10. lemma OAI.WeakPureInfiniteness.oInfinity_hom_ext line 130