English
Let a, b, c be noncollinear points in a Euclidean geometry. Then the shorter side opposite angle ∠ACB corresponds to a smaller angle ∠ABC; equivalently, AB < AC if and only if ∠ACB < ∠ABC.
Русский
Пусть a, b, c — неколлинеарные точки в евклидовом пространстве. Тогда меньшая противолежащая сторона соответствует меньшему углу напротив неё: AB < AC эквивалентно ⟨ACB⟩ < ⟨ABC⟩.
LaTeX
$$$\forall a,b,c \in P,\; \neg\mathrm{Collinear}(a,b,c) \Rightarrow \left( \angle a c b < \angle a b c \;\Longleftrightarrow\; \operatorname{dist}(a,b) < \operatorname{dist}(a,c) \right)$$$
Lean4
theorem angle_lt_iff_dist_lt {a b c : P} (h : ¬Collinear ℝ ({ a, b, c } : Set P)) :
∠ a c b < ∠ a b c ↔ dist a b < dist a c := by
constructor
case mp => exact dist_lt_of_angle_lt h
case mpr =>
intro h1
by_contra! w
rcases w.eq_or_lt with h2 | h3
· have h4 : dist a b = dist a c :=
by
apply dist_eq_of_angle_eq_angle_of_angle_ne_pi h2
rw [show ({ a, b, c } : Set P) = { b, a, c } by exact Set.insert_comm a b { c }] at h
linarith [angle_lt_pi_of_not_collinear h]
linarith
· rw [show ({ a, b, c } : Set P) = { a, c, b } by grind] at h
have h5 := dist_lt_of_angle_lt h h3
linarith
