OAI/Analysis/Cotype/ComplexDualLift.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Cotype.ComplexDualSpace line 11
  2. instance OAI.Cotype.complexDualSpaceNormedAddCommGroup line 14
  3. instance OAI.Cotype.complexDualSpaceNormedSpace line 17
  4. def OAI.Cotype.realDualAction line 20
  5. theorem OAI.Cotype.realDualAction_apply line 27
  6. theorem OAI.Cotype.realDualAction_norm_le line 30
  7. def OAI.Cotype.complexDualLift line 35
  8. theorem OAI.Cotype.complexDualLift_apply line 43
  9. theorem OAI.Cotype.complexDualLift_norm_le line 47
  10. def OAI.Cotype.complexDualEmbed line 53
  11. theorem OAI.Cotype.complexDualEmbed_apply line 56
  12. theorem OAI.Cotype.complexDualEmbed_norm line 59
  13. theorem OAI.Cotype.complexDualLift_embed line 70
  14. theorem OAI.Cotype.complexDualLift_norm line 75
  15. theorem OAI.Cotype.complexDualLift_one line 82
  16. theorem OAI.Cotype.complexDualLift_mul line 87
  17. theorem OAI.Cotype.complexDualLift_add line 92
  18. theorem OAI.Cotype.complexDualLift_sub line 98
  19. theorem OAI.Cotype.complexDualLift_smul line 104
  20. theorem OAI.Cotype.complexDualLift_pow line 110
  21. theorem OAI.Cotype.complexDualLift_power_gap line 116