structure Geodesics.IsMetricGeodesicSegment {X : Type u_1} [MetricSpace X] (γ : ℝ → X) (p q : X) : Prop

• source : γ 0 = p
• target : γ 1 = q
• proportional (s t : ℝ) : s ∈ Set.Icc 0 1 → t ∈ Set.Icc 0 1 → dist (γ s) (γ t) = |t - s| * dist p q

structure Geodesics.GeodesicTriangle (X : Type u_1) [MetricSpace X] : Type u_1

• p₁ : X
• p₂ : X
• p₃ : X
• γ₁₂ : ℝ → X
• γ₂₃ : ℝ → X
• γ₁₃ : ℝ → X
• isGeodesic₁₂ : IsMetricGeodesicSegment self.γ₁₂ self.p₁ self.p₂
• isGeodesic₂₃ : IsMetricGeodesicSegment self.γ₂₃ self.p₂ self.p₃
• isGeodesic₁₃ : IsMetricGeodesicSegment self.γ₁₃ self.p₁ self.p₃

def Geodesics.GeodesicTriangle.sideA {X : Type u_1} [MetricSpace X] (T : GeodesicTriangle X) : ℝ

def Geodesics.GeodesicTriangle.sideB {X : Type u_1} [MetricSpace X] (T : GeodesicTriangle X) : ℝ

def Geodesics.GeodesicTriangle.sideC {X : Type u_1} [MetricSpace X] (T : GeodesicTriangle X) : ℝ

noncomputable def Geodesics.comparisonAngle {X : Type u_1} [MetricSpace X] (p₁ p₂ p₃ : X) : ℝ

noncomputable def Geodesics.GeodesicTriangle.comparisonAngleAt₁ {X : Type u_1} [MetricSpace X] (T : GeodesicTriangle X) : ℝ

noncomputable def Geodesics.GeodesicTriangle.comparisonAngleAt₂ {X : Type u_1} [MetricSpace X] (T : GeodesicTriangle X) : ℝ

noncomputable def Geodesics.GeodesicTriangle.comparisonAngleAt₃ {X : Type u_1} [MetricSpace X] (T : GeodesicTriangle X) : ℝ

structure Geodesics.ComparisonTriangle (X : Type u_1) [MetricSpace X] (T : GeodesicTriangle X) : Type

• q₁ : EuclideanSpace ℝ (Fin 2)
• q₂ : EuclideanSpace ℝ (Fin 2)
• q₃ : EuclideanSpace ℝ (Fin 2)
• dist_eq₁₂ : dist self.q₁ self.q₂ = dist T.p₁ T.p₂
• dist_eq₂₃ : dist self.q₂ self.q₃ = dist T.p₂ T.p₃
• dist_eq₁₃ : dist self.q₁ self.q₃ = dist T.p₁ T.p₃