OAI/Analysis/Commutator/FiberFactorProducer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.Decomposable.fieldMember_mono line 27
2. def OAI.Kadison.Decomposable.fiberJoin line 35
3. lemma OAI.Kadison.Decomposable.le_fiberJoin_left line 39
4. lemma OAI.Kadison.Decomposable.le_fiberJoin_right line 46
5. lemma OAI.Kadison.Decomposable.factor_of_rankOne_mem_join line 53
6. theorem OAI.Kadison.Decomposable.factors_ae_of_central_geometry line 65