angle_coe — Mathlib

English

If p1,p2,p3 are points in an affine subspace s, then the angle computed in s equals the ambient angle.

Русский

Если p1,p2,p3 лежат в аффинном подпространстве s, тот же угол вычисляется внутри s и в окружающем пространстве одинаково.

LaTeX

$$$\angle p_1 p_2 p_3 = \angle (p_1 : P) (p_2 : P) (p_3 : P)$, для точек в s.$$

Lean4

@[simp, norm_cast]
theorem _root_.AffineSubspace.angle_coe {s : AffineSubspace ℝ P} (p₁ p₂ p₃ : s) :
    haveI : Nonempty s := ⟨p₁⟩
    ∠ (p₁ : P) (p₂ : P) (p₃ : P) = ∠ p₁ p₂ p₃ :=
  haveI : Nonempty s := ⟨p₁⟩
  s.subtypeₐᵢ.angle_map p₁ p₂ p₃

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