eq_neg_swap — Mathlib

English

variationOnFromTo f s a b = - variationOnFromTo f s b a.

Русский

variationOnFromTo f s a b = - variationOnFromTo f s b a.

LaTeX

$$variationOnFromTo f s a b = - variationOnFromTo f s b a$$

Lean4

protected theorem eq_neg_swap (a b : α) : variationOnFromTo f s a b = -variationOnFromTo f s b a :=
  by
  rcases lt_trichotomy a b with (ab | rfl | ba)
  · simp only [variationOnFromTo, if_pos ab.le, if_neg ab.not_ge, neg_neg]
  · simp only [variationOnFromTo.self, neg_zero]
  · simp only [variationOnFromTo, if_pos ba.le, if_neg ba.not_ge]

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