neg — Mathlib

English

If a is related to b by r, then their negatives are related by r as well.

Русский

Если a связано с b отношением r, то их отрицания также связаны отношением r.

LaTeX

$$$\\forall a,b,\\; \\mathrm{Rel}\\ r\\ a\\ b \\Rightarrow \\mathrm{Rel}\\ r\\ (-a)\\ (-b).$$$

Lean4

theorem neg {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : Rel r a b) : Rel r (-a) (-b) := by
  simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, Rel.mul_right h]

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