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₃