OAI/Geometry/SplitTangent/LeafJetAtlas.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Leaf Jet Atlas.

  1. structure OAI.SplitTangent.LeafJetAtlas line 20
  2. def OAI.SplitTangent.TangentSplitting.leafJetAtlas line 24
  3. abbrev OAI.SplitTangent.LeafJetAtlas.jet line 32
  4. lemma OAI.SplitTangent.LeafJetAtlas.jet_add line 35
  5. lemma OAI.SplitTangent.LeafJetAtlas.jet_csmul line 41
  6. lemma OAI.SplitTangent.LeafJetAtlas.jet_zero line 46
  7. lemma OAI.SplitTangent.LeafJetAtlas.jet_smul line 49
  8. lemma OAI.SplitTangent.LeafJetAtlas.jet_congr line 56
  9. lemma OAI.SplitTangent.LeafJetAtlas.parameter_slice line 60
  10. theorem OAI.SplitTangent.LeafJetAtlas.leading_analytic line 67
  11. lemma OAI.SplitTangent.LeafJetAtlas.jet_supported line 83
  12. lemma OAI.SplitTangent.LeafJetAtlas.jet_symmetric line 88