Triangles are compact and lie in every half-plane containing their vertices

Closed sides and triangles are convex: they contain the geodesic segment between any two of their points (geodesicSegment_subset_closedSide, geodesicSegment_subset_triangle). A nondegenerate triangle is compact (isCompact_triangle), its trace on the line through two vertices is the side between them (triangle_inter_range_geodesicLine), and it lies in every closed half-plane containing its three vertices (triangle_subset_closure_leftHalfPlane, triangle_subset_closure_rightHalfPlane): the triangle defined as an intersection of three closed sides is the convex hull of its vertices.

The file also records basic facts about closed sides and triangles that the above needs: a closed side is the closed half-plane of its reference point when that point is off the line (closedSide_eq_closure_leftHalfPlane_of_mem, closedSide_eq_closure_rightHalfPlane_of_mem), and the frontiers of a closed side and of a triangle lie on the bounding lines (UpperHalfPlane.frontier_closedSide_subset, UpperHalfPlane.frontier_triangle_subset).

Source: Walkden, Hyperbolic geometry (MATH32051), §14.2 (convex polygons as intersections of half-planes); Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), p. 20 (the angular defect). The hull statement is evident in the sources; the proof is ours.

The frontiers of closed sides and triangles

theorem UpperHalfPlane.frontier_closedSide_subset (z w u : UpperHalfPlane) : frontier (z.closedSide w u) ⊆ Set.range (TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween z w))

The frontier of a closed side lies on its bounding line.

theorem UpperHalfPlane.frontier_triangle_subset (A B C : UpperHalfPlane) : frontier (A.triangle B C) ⊆ Set.range (TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween A B)) ∪ Set.range (TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween B C)) ∪ Set.range (TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween C A))

The frontier of a triangle lies on the union of its three side lines.

Closed sides and triangles

theorem TauCeti.UpperHalfPlane.closedSide_eq_closure_leftHalfPlane_of_mem {z w u : UpperHalfPlane} (hu : u ∈ leftHalfPlane (geodesicBetween z w)) : z.closedSide w u = closure (leftHalfPlane (geodesicBetween z w))

The closed side containing a point of the open left half-plane is the closed left half-plane.

theorem TauCeti.UpperHalfPlane.closedSide_eq_closure_rightHalfPlane_of_mem {z w u : UpperHalfPlane} (hu : u ∈ rightHalfPlane (geodesicBetween z w)) : z.closedSide w u = closure (rightHalfPlane (geodesicBetween z w))

The closed side containing a point of the open right half-plane is the closed right half-plane.

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_closedSide {u v x z w : UpperHalfPlane} (hz : z ∈ u.closedSide v x) (hw : w ∈ u.closedSide v x) : z.geodesicSegment w ⊆ u.closedSide v x

Closed sides are convex.

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_triangle {A B C z w : UpperHalfPlane} (hz : z ∈ A.triangle B C) (hw : w ∈ A.triangle B C) : z.geodesicSegment w ⊆ A.triangle B C

Triangles are convex.

The trace of a triangle on a side line

theorem TauCeti.UpperHalfPlane.triangle_inter_range_geodesicLine {A B C : UpperHalfPlane} (hAB : A ≠ B) (hC : C ∉ Set.range (geodesicLine (geodesicBetween A B))) : A.triangle B C ∩ Set.range (geodesicLine (geodesicBetween A B)) = A.geodesicSegment B

The trace of a nondegenerate triangle on the line through two of its vertices is the side between them.

Compactness

theorem TauCeti.UpperHalfPlane.isCompact_triangle {A B C : UpperHalfPlane} (hAB : A ≠ B) (hC : C ∉ Set.range (geodesicLine (geodesicBetween A B))) : IsCompact (A.triangle B C)

Nondegenerate triangles are compact.

The hull property

theorem TauCeti.UpperHalfPlane.triangle_subset_closure_leftHalfPlane {A B C : UpperHalfPlane} (hAB : A ≠ B) (hC : C ∉ Set.range (geodesicLine (geodesicBetween A B))) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hA : A ∈ closure (leftHalfPlane g)) (hB : B ∈ closure (leftHalfPlane g)) (hC' : C ∈ closure (leftHalfPlane g)) : A.triangle B C ⊆ closure (leftHalfPlane g)

A nondegenerate triangle lies in every closed left half-plane containing its vertices.

theorem TauCeti.UpperHalfPlane.triangle_subset_closure_rightHalfPlane {A B C : UpperHalfPlane} (hAB : A ≠ B) (hC : C ∉ Set.range (geodesicLine (geodesicBetween A B))) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hA : A ∈ closure (rightHalfPlane g)) (hB : B ∈ closure (rightHalfPlane g)) (hC' : C ∈ closure (rightHalfPlane g)) : A.triangle B C ⊆ closure (rightHalfPlane g)

A nondegenerate triangle lies in every closed right half-plane containing its vertices.

The angular defect