OAI/Analysis/Commutator/FiniteSupportFactorization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorFunctionals.extendOperator line 22
2. lemma OAI.Kadison.OperatorFunctionals.extendOperator_apply line 37
3. lemma OAI.Kadison.OperatorFunctionals.extendOperator_norm line 44
4. def OAI.Kadison.OperatorFunctionals.finiteFunctional line 49
5. lemma OAI.Kadison.OperatorFunctionals.finiteFunctional_apply line 53
6. lemma OAI.Kadison.OperatorFunctionals.tuple_coe_norm line 58
7. theorem OAI.Kadison.OperatorFunctionals.exists_finite_support_factorization line 64