OAI/Topology/ArtinGroups/Harmonic/ConeAttachmentRel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.HarmonicArtin.ConeAttachmentRel line 12
  2. abbrev OAI.HarmonicArtin.ConeAttachment line 16
  3. def OAI.HarmonicArtin.coneAttachmentOld line 18
  4. def OAI.HarmonicArtin.coneAttachmentCone line 21
  5. lemma OAI.HarmonicArtin.coneAttachment_base line 24
  6. lemma OAI.HarmonicArtin.coneAttachment_apex line 27
  7. lemma OAI.HarmonicArtin.continuous_prod_sum_elim line 30
  8. def OAI.HarmonicArtin.coneAttachmentRetract line 43
  9. lemma OAI.HarmonicArtin.coneAttachmentRetract_old line 51
  10. def OAI.HarmonicArtin.coneAttachmentMiddle line 54
  11. def OAI.HarmonicArtin.coneAttachmentFirstFun line 63
  12. def OAI.HarmonicArtin.coneAttachmentFirst line 72
  13. def OAI.HarmonicArtin.coneAttachmentSecondFun line 101
  14. def OAI.HarmonicArtin.coneAttachmentSecond line 110
  15. def OAI.HarmonicArtin.coneAttachmentDeformation line 142
  16. def OAI.HarmonicArtin.coneAttachmentEquiv line 148