OAI/Analysis/Cotype/CoefficientCompactness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Cotype.ScalarTriple line 12
  2. def OAI.Cotype.admissibleSet line 14
  3. theorem OAI.Cotype.admissibleSet_closed line 17
  4. theorem OAI.Cotype.function_box_compact line 27
  5. theorem OAI.Cotype.admissibleSet_compact line 33
  6. def OAI.Cotype.rankTwoMax line 43
  7. theorem OAI.Cotype.rankTwoMax_continuous line 47
  8. theorem OAI.Cotype.rankTwoMax_pos line 57
  9. theorem OAI.Cotype.rankTwoMax_attained line 65
  10. theorem OAI.Cotype.coefficientTarget_proved line 74