OAI/Geometry/SplitTangent/TangentRationalChains.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Tangent Rational Chains.

  1. def OAI.SplitTangent.RationalCurve.TangentTo line 18
  2. def OAI.SplitTangent.TangentBox.horizontal line 28
  3. lemma OAI.SplitTangent.TangentBox.horizontal_derivative line 39
  4. lemma OAI.SplitTangent.TangentBox.horizontal_tangent line 53
  5. lemma OAI.SplitTangent.TangentBox.vertical_rational_tangent line 62
  6. def OAI.SplitTangent.TangentRationalRelated line 68
  7. def OAI.SplitTangent.TangentChainRelated line 74
  8. lemma OAI.SplitTangent.TangentRationalRelated.symm line 78
  9. theorem OAI.SplitTangent.TangentSplitting.two_tangent_curves_of_rational line 86
  10. lemma OAI.SplitTangent.TangentChainRelated.refl line 100
  11. lemma OAI.SplitTangent.TangentChainRelated.trans line 104
  12. lemma OAI.SplitTangent.TangentChainRelated.symm line 109
  13. def OAI.SplitTangent.tangentChainSetoid line 117
  14. theorem OAI.SplitTangent.TangentSplitting.general_mixed_tangent_curves line 124