term∠ — Mathlib

English

For a point-vertex pair in an affine subspace s, the angle measured in s agrees with the angle measured in the ambient space P.

Русский

Для точки-вершины в аффинном подпространстве s угол, измеряемый в s, совпадает с углом в окружающем пространстве P.

LaTeX

$$$\angle (p_1 : P) (p_2 : P) (p_3 : P) = \angle p_1 p_2 p_3$ для $p_1,p_2,p_3 \in s$ и не пустого s.$$

Lean4

@[inherit_doc EuclideanGeometry.angle, scoped term_parser 1000]
public meta def «term∠» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `EuclideanGeometry.«term∠» 1024 (ParserDescr.symbol✝ "∠")

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