Documentation

TauCeti.Analysis.Complex.UpperHalfPlane.Geodesic.InteriorAngle

The angle at a point between the geodesics towards two other points #

UpperHalfPlane.interiorAngle A B C is the angle at A between the geodesics from A to B and from A to C: the angle geodesicAngle between the geodesic lines geodesicBetween A B and geodesicBetween A C. It is symmetric in B and C (UpperHalfPlane.interiorAngle_comm), lies in [0, π] (UpperHalfPlane.interiorAngle_nonneg, UpperHalfPlane.interiorAngle_le_pi), and is invariant under PSL(2, ℝ) when A ≠ B and A ≠ C (interiorAngle_smul). It is the interior angle of hyperbolic triangles and polygons.

source
noncomputable def UpperHalfPlane.interiorAngle (A B C : UpperHalfPlane) :
ℝ

The interior angle at A between the directions to B and to C: the angle between the geodesics from A to B and from A to C.

Equations
Instances For
    source
    theorem UpperHalfPlane.interiorAngle_def (A B C : UpperHalfPlane) :
    A.interiorAngle B C = TauCeti.UpperHalfPlane.geodesicAngle (TauCeti.UpperHalfPlane.geodesicBetween A B) (TauCeti.UpperHalfPlane.geodesicBetween A C)

    interiorAngle is the angle between the geodesics from A to B and from A to C.

    source
    theorem UpperHalfPlane.interiorAngle_comm (A B C : UpperHalfPlane) :
    A.interiorAngle C B = A.interiorAngle B C

    The interior angle at A does not depend on the order of the other two vertices.

    source
    theorem UpperHalfPlane.interiorAngle_nonneg (A B C : UpperHalfPlane) :
    0 ≤ A.interiorAngle B C

    Interior angles are nonnegative.

    source
    theorem UpperHalfPlane.interiorAngle_le_pi (A B C : UpperHalfPlane) :
    A.interiorAngle B C ≤ Real.pi

    Interior angles are at most π.

    source
    theorem TauCeti.UpperHalfPlane.interiorAngle_smul (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {A B C : UpperHalfPlane} (hAB : A ≠ B) (hAC : A ≠ C) :
    (h • A).interiorAngle (h • B) (h • C) = A.interiorAngle B C

    Interior angles at A are invariant under the action, for A ≠ B and A ≠ C.