excenterExists_compl

Mathlib.Geometry.Euclidean.Incenter

URI: https://scilib.ai/kg/mathlib#Affine.Simplex.excenterExists_compl

English

Excenter exists equivalence under complement of signs (symmetry).

Русский

Существование эксцентра эквивалентно комплементу знаков.

LaTeX

$$$s.ExcenterExists(signs^c) \iff s.ExcenterExists(signs)$$$

Lean4

@[simp]
theorem excenterExists_compl {signs : Finset (Fin (n + 1))} : s.ExcenterExists signsᶜ ↔ s.ExcenterExists signs := by
  simp [ExcenterExists]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru