OAI/Geometry/ProjectionBody/GraphChart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProjectionCounterexample.graphLinear line 12

   Source documentation

   A graph chart with one coordinate determined by a linear equation.

   def graphLinear {n : ℕ} (i : Fin (n + 1)) (a : E n) : E n →ₗ[ℝ] E (n + 1) where
   …

   Mentions: OAI.ProjectionCounterexample.E

2. def OAI.ProjectionCounterexample.graphNormal line 21

   Source documentation

   The corresponding unnormalized normal has coordinate i equal to one.

   def graphNormal {n : ℕ} (i : Fin (n + 1)) (a : E n) : E (n + 1) :=
   …

   Mentions: OAI.ProjectionCounterexample.E

3. theorem OAI.ProjectionCounterexample.graphNormal_same line 24
4. theorem OAI.ProjectionCounterexample.graphNormal_ne_zero line 27
5. theorem OAI.ProjectionCounterexample.graphLinear_same line 33
6. theorem OAI.ProjectionCounterexample.graphLinear_succAbove line 36
7. theorem OAI.ProjectionCounterexample.graphLinear_inner line 40
8. theorem OAI.ProjectionCounterexample.graphNormal_inner_graphLinear line 46
9. theorem OAI.ProjectionCounterexample.graphNormal_norm_sq line 52