OAI/Geometry/SplitTangent/ProjectiveLinearCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Projective Linear Coordinates.

  1. def OAI.ProjectiveLinearCoordinates.form line 18
  2. lemma OAI.ProjectiveLinearCoordinates.eval_form line 22
  3. lemma OAI.ProjectiveLinearCoordinates.eval_form_ratio line 36
  4. lemma OAI.SplitTangent.ProjectiveEmbedding.plaque_coordinates_analytic line 49
  5. lemma OAI.SplitTangent.ProjectiveEmbedding.plaque_coordinates_first_injective line 57
  6. lemma OAI.SplitTangent.ProjectiveEmbedding.coordinates_injOn line 72
  7. theorem OAI.SplitTangent.ProjectiveEmbedding.exists_linear_plaque_coordinates line 91