Theorems · Theorem · geometry

EuclideanGeometry.dist_lt_of_angle_lt

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P},
  ¬Collinear ℝ {a, b, c} → EuclideanGeometry.angle a c b < EuclideanGeometry.angle a b c → dist a b < dist a c

In a triangle, the smaller angle is opposite the smaller side.

Defined in

Mathlib.Geometry.Euclidean.Triangle

Cited by

1 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor