OAI/Analysis/Cotype/TypeCotypeDuality.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Cotype.HasType line 13
2. def OAI.Cotype.NontrivialType line 17
3. theorem OAI.Cotype.tuple_dual_lq_le line 20
4. theorem OAI.Cotype.dualPairing_rademacherSum line 80
5. theorem OAI.Cotype.hasCotype_dual_of_hasType line 90
6. theorem OAI.Cotype.hasCotype_of_linearIsometry line 104
7. theorem OAI.Cotype.hasCotype_of_bidual line 112
8. theorem OAI.Cotype.finiteCotype_pair_of_nontrivialType line 116