symmAt — Mathlib

English

Reversal of a GenLoop along the i-th coordinate: flip the order along the i-th axis, leaving other coordinates unchanged.

Русский

Переоборот GenLoop вдоль i-й координаты: разворот по оси i, прочие координаты остаются без изменений.

LaTeX

$$$\\mathrm{symmAt}(i; f)\\;:\\; Ω^N X x \\to Ω^N X x$$$

Lean4

/-- Reversal of a `GenLoop` along the `i`th coordinate. -/
def symmAt (i : N) (f : Ω^ N X x) : Ω^ N X x :=
  (copy (fromLoop i (toLoop i f).symm) fun t => f fun j => if j = i then σ (t i) else t j) <| by ext1; change _ = f _;
    congr; ext1; simp

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