OAI/Geometry/SurfaceImmersion/Primitive/BoundaryProfileNormal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The preferred and complementary normals of a regular five-profile.

  1. lemma OAI.ClosedSurfaceR4.GeometryPreservation.profilePreferred_unit line 12
  2. lemma OAI.ClosedSurfaceR4.GeometryPreservation.profilePreferred_perp line 15
  3. lemma OAI.ClosedSurfaceR4.GeometryPreservation.profileComplement_unit line 20
  4. lemma OAI.ClosedSurfaceR4.GeometryPreservation.profileComplement_perp line 25
  5. lemma OAI.ClosedSurfaceR4.GeometryPreservation.profileComplement_abs_dot line 31

    Source documentation

    Every unit normal orthogonal to the preferred normal reads the same absolute complementary coefficient, regardless of the orientation choice.

    lemma profileComplement_abs_dot {J : BoundaryProfile} (hJ : J ∈ regularBoundaryProfiles)
    {u : Vec} (hu : u ⬝ᵥ u = 1) (hXu : J 0 ⬝ᵥ u = 0) (hYu : J 1 ⬝ᵥ u = 0)
    (hnu : profilePreferred J ⬝ᵥ u = 0) (W : Vec) :
    |W ⬝ᵥ profileComplement J| = |W ⬝ᵥ u| := by
…

    Mentions: OAI.ClosedSurfaceR4.GeometryPreservation.BoundaryProfile, OAI.ClosedSurfaceR4.GeometryPreservation.regularBoundaryProfiles, OAI.ClosedSurfaceR4.GeometryPreservation.profilePreferred, OAI.ClosedSurfaceR4.GeometryPreservation.profileComplement