negAddY_neg — Mathlib

English

For any P, Q, the relation negAddY P (neg Q) yields the same as dblZ P, highlighting a fundamental identity in the negation operations.

Русский

Для любых P, Q выражение negAddYP (neg Q) даёт тот же результат, что и dblZ P, подчёркивая фундаментальную идентичность операций отрицания.

LaTeX

$$$$\text{negAddY} P \bigl(\text{neg} P\bigr) = \text{dblZ} P$$$$

Lean4

theorem negAddY_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.negAddY P (W'.neg P) = W'.dblZ P := by
  linear_combination (norm := (rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -3 * (P y - W'.negY P) * (equation_iff _).mp hP

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