OAI/Analysis/AffineBernstein/CapCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.equivMatrix line 11
2. lemma OAI.AffineBernstein.toEuclideanCLM_equivMatrix line 15
3. lemma OAI.AffineBernstein.equivMatrix_det_ne line 21
4. lemma OAI.AffineBernstein.equivMatrix_det line 25
5. def OAI.AffineBernstein.cleGraphPullback line 29
6. lemma OAI.AffineBernstein.cleGraphPullback_eq line 33
7. lemma OAI.AffineBernstein.cleGraphPullback_regular line 40
8. def OAI.AffineBernstein.verticalShear line 61

   Source documentation

   A shear does not change height and straightens an upward vector.

   def verticalShear {n : ℕ} (p : Space n) : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ) :=
   …

   Mentions: OAI.AffineBernstein.Space

9. lemma OAI.AffineBernstein.verticalShear_apply line 70
10. lemma OAI.AffineBernstein.verticalShear_straightens line 73
11. lemma OAI.AffineBernstein.vertical_map line 77
12. lemma OAI.AffineBernstein.triangular_fst line 83
13. lemma OAI.AffineBernstein.triangular_snd line 90
14. lemma OAI.AffineBernstein.triangular_symm_vertical line 97
15. def OAI.AffineBernstein.triangularBaseEquiv line 104

    Source documentation

    The induced invertible horizontal map of a triangular ambient affine map.

    def triangularBaseEquiv {n : ℕ} (M : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ))
        {c : ℝ} (hc : M (0,1) = (0,c)) (hcn : c ≠ 0) : Space n ≃L[ℝ] Space n :=
    …

    Mentions: OAI.AffineBernstein.Space

16. lemma OAI.AffineBernstein.triangularBaseEquiv_apply line 120
17. lemma OAI.AffineBernstein.triangularBaseEquiv_symm_apply line 125