pointsWithCircumcenter_eq_circumcenter

English

The circumcenter can be obtained as the special evaluation of pointsWithCircumcenter at circumcenterIndex.

Русский

Центр описанной окружности достигается как особое значение pointsWithCircumcenter в circumcenterIndex.

LaTeX

$$$s.circumcenter = (\mathrm{pointsWithCircumcenter}\,s)(\text{circumcenterIndex})$$$

Lean4

/-- `pointsWithCircumcenter`, applied to `circumcenterIndex`, equals the
circumcenter. -/
@[simp]
theorem pointsWithCircumcenter_eq_circumcenter {n : ℕ} (s : Simplex ℝ P n) :
    s.pointsWithCircumcenter circumcenterIndex = s.circumcenter :=
  rfl

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