OAI/Analysis/JiangSu/CentralSequences/QuasicentralFinite.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Quasicentral.exists_strict_ideal_contraction line 16
2. lemma OAI.Quasicentral.ideal_conjugate_mem line 41
3. theorem OAI.Quasicentral.exists_quasicentral_unitary_contraction line 45
4. theorem OAI.Quasicentral.exists_quasicentral_contraction line 60
5. def OAI.Quasicentral.unitizedKernel line 106
6. lemma OAI.Quasicentral.unitizedKernel_mem line 118
7. lemma OAI.Quasicentral.inr_mem_unitizedKernel line 126
8. theorem OAI.Quasicentral.exists_quasicentral_kernel_contraction line 131