OAI/Analysis/TracialSplitting/SmallProjections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentMain.full_of_complement_bound line 30
2. theorem OAI.CurrentMain.small_full_projections line 54