OAI/Analysis/Cotype/UniformL1.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Cotype.L1Family line 11
2. def OAI.Cotype.UniformL1 line 14
3. theorem OAI.Cotype.L1Family.upper line 17
4. theorem OAI.Cotype.L1Family.reindex line 24
5. theorem OAI.Cotype.L1Family.restrict line 31
6. theorem OAI.Cotype.uniformL1_iff_cube line 55
7. theorem OAI.Cotype.not_uniformL1_of_no_cube line 73