mlieBracketWithin_swap_apply — Mathlib

English

The swap of V and W in the Lie bracket within relates to the negation: mlieBracketWithin_swap_apply gives that bracket with swapped fields is negated.

Русский

Замена V и W в скобке Ли внутри даёт отрицание скобки при перестановке полей.

LaTeX

$$mlieBracketWithin_swap_apply : mlieBracketWithin I V W s x = -mlieBracketWithin I W V s x$$

Lean4

theorem mlieBracketWithin_swap_apply : mlieBracketWithin I V W s x = -mlieBracketWithin I W V s x :=
  by
  rw [mlieBracketWithin, lieBracketWithin_swap, mpullback_neg]
  rfl

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