OAI/Analysis/WeakInfiniteness/SeparationPreassembly.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.unitizedRight line 30
2. lemma OAI.WeakPureInfiniteness.inr_unitizedRight line 33
3. lemma OAI.WeakPureInfiniteness.inr_factor_mem_principal line 36
4. lemma OAI.WeakPureInfiniteness.inr_separationG line 46
5. lemma OAI.WeakPureInfiniteness.inr_separationN line 52
6. lemma OAI.WeakPureInfiniteness.norm_separationG line 58