signBijAux — Mathlib

English

Sign of the auxiliary bijection on a finite pair depends on the order of the pair determined by f.

Русский

Знак вспомогательной биекции на конечной паре зависит от порядка пары, заданного f.

LaTeX

$$$ \\mathrm{signBijAux}(f, a) = \\begin{cases} (f a.1, f a.2), & f a.2 < f a.1 \\\\ (f a.2, f a.1), & \\text{otherwise} \\end{cases} $$$

Lean4

/-- `signBijAux f ⟨a, b⟩` returns the pair consisting of `f a` and `f b` in decreasing order. -/
def signBijAux {n : ℕ} (f : Perm (Fin n)) (a : Σ _ : Fin n, Fin n) : Σ _ : Fin n, Fin n :=
  if _ : f a.2 < f a.1 then ⟨f a.1, f a.2⟩ else ⟨f a.2, f a.1⟩

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