OAI/Geometry/RuledCovering/Isometries.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RuledApproximation.IsParallelogram.translate line 12
2. def OAI.RuledApproximation.rotatedPlane line 24
3. def OAI.RuledApproximation.Cylinder.rotate line 40
4. lemma OAI.RuledApproximation.Cylinder.rotate_carrier line 45
5. lemma OAI.RuledApproximation.Cylinder.rotate_area line 54
6. lemma OAI.RuledApproximation.Cylinder.rotate_parallelogram line 61
7. def OAI.RuledApproximation.Cylinder.transversePart line 65
8. def OAI.RuledApproximation.Cylinder.translate line 72
9. lemma OAI.RuledApproximation.Cylinder.translate_carrier line 77
10. lemma OAI.RuledApproximation.Cylinder.translate_area line 93
11. lemma OAI.RuledApproximation.Cylinder.translate_parallelogram line 100
12. lemma OAI.RuledApproximation.HasFiniteCover.isometry line 104

    Source documentation

    Exact Euclidean isometry transport preserves finite covers and perpendicular area.

    lemma HasFiniteCover.isometry {S : Set Space} {A : ℝ}
        (hc : HasFiniteCover Cylinder.parallelogram S A) (F : Space ≃ᵢ Space) :
        HasFiniteCover Cylinder.parallelogram (F '' S) A := by
    …

    Mentions: OAI.RuledApproximation.Space, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.Cylinder.parallelogram