oangle_eq_right — Mathlib

English

If p2, p3, p3' lie in weak betweenness and p3 ≠ p2, then ∡ p1 p2 p3 = ∡ p1 p2 p3'.

Русский

Если p2, p3, p3' лежат в слабом отношении между собой и p3 ≠ p2, то угол остаётся неизменным: ∡ p1 p2 p3 = ∡ p1 p2 p3'.

LaTeX

$$$Wbtw_\mathbb{R}(p_2,p_3,p_3') \land p_3' \neq p_2 \Rightarrow \angle p_1 p_2 p_3 = \angle p_1 p_2 p_3'$$$

Lean4

/-- An oriented angle is unchanged by replacing the third point by one weakly further away on the
same ray. -/
theorem _root_.Wbtw.oangle_eq_right {p₁ p₂ p₃ p₃' : P} (h : Wbtw ℝ p₂ p₃ p₃') (hp₃p₂ : p₃ ≠ p₂) :
    ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' := by rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]

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