excenterWeightsUnnorm_compl — Mathlib

English

Excenter existence is invariant under complement of the sign set.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem excenterWeightsUnnorm_compl (signs : Finset (Fin (n + 1))) :
    s.excenterWeightsUnnorm signsᶜ = -s.excenterWeightsUnnorm signs :=
  by
  ext i
  by_cases h : i ∈ signs <;> simp [excenterWeightsUnnorm, h]

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