angle_le_iff_dist_le — Mathlib

English

Let a, b, c be noncollinear points. Then ∠ACB ≤ ∠ABC if and only if AB ≤ AC.

Русский

Пусть a, b, c — неколлинеарные точки. Тогда ∠ACB ≤ ∠ABC тогда и только тогда, когда AB ≤ AC.

LaTeX

$$$\forall a,b,c \in P,\; \neg\mathrm{Collinear}(a,b,c) \Rightarrow \left( \angle a c b \le \angle a b c \;\Longleftrightarrow\; \operatorname{dist}(a,b) \le \operatorname{dist}(a,c) \right)$$$

Lean4

theorem angle_le_iff_dist_le {a b c : P} (h : ¬Collinear ℝ ({ a, b, c } : Set P)) :
    ∠ a c b ≤ ∠ a b c ↔ dist a b ≤ dist a c :=
  by
  rw [show ({ a, b, c } : Set P) = { a, c, b } by grind] at h
  simpa using (angle_lt_iff_dist_lt h).not

Похожие утверждения