OAI/Analysis/WeakInfiniteness/NonunitalSpectralTools2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.map_mem_hereditary line 27
2. lemma OAI.WeakPureInfiniteness.continuouslySupported_hereditary_nonunital line 37
3. def OAI.WeakPureInfiniteness.unitizationSubalgebra line 45
4. lemma OAI.WeakPureInfiniteness.unitizationSubalgebra_closed line 54
5. lemma OAI.WeakPureInfiniteness.unitizationSubalgebra_inr_mem line 58
6. lemma OAI.WeakPureInfiniteness.unitization_inr_snd_of_fst_eq_zero line 62