OAI/Analysis/C0Absorption/Absorption.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.absorptionK line 14
  2. def OAI.C0Absorption.absorptionG line 15
  3. theorem OAI.C0Absorption.absorptionK_lipschitz line 17
  4. theorem OAI.C0Absorption.absorptionG_surjective line 24
  5. theorem OAI.C0Absorption.absorptionG_lower line 27
  6. theorem OAI.C0Absorption.absorptionQK line 34
  7. def OAI.C0Absorption.concreteAbsorption line 40
  8. theorem OAI.C0Absorption.concreteAbsorption_surjective line 42
  9. theorem OAI.C0Absorption.concreteAbsorption_upper line 45
  10. theorem OAI.C0Absorption.concreteAbsorption_inverse_bound line 49
  11. theorem OAI.C0Absorption.concreteAbsorption_bilip line 55
  12. def OAI.C0Absorption.concreteC0Embedding line 66
  13. theorem OAI.C0Absorption.concreteC0Embedding_bilip line 68
  14. theorem OAI.C0Absorption.noLinearC0_not_product_equiv line 73
  15. theorem OAI.C0Absorption.concrete_not_linearly_isomorphic line 90