getElem_leftInvSeq — Mathlib

English

For ω and j with a suitable bound, the j-th element of lis ω relates to a π-product and a conjugation by s ω[j].

Русский

Для ω и j при условии, что индекс корректен, j-й элемент lis ω связан с произведением π и сопряжением конъюга по s ω[j].

LaTeX

$$$(\mathrm{lis}(\omega))[j]' = (\pi(\omega.take j)) \cdot ((\mathrm{Option.map}(\mathrm{cs.simple}) (\omega[j]?)).getD 1) \cdot (\pi(\omega.take j))^{-1}$$$

Lean4

theorem getElem_leftInvSeq (ω : List B) (j : ℕ) (h : j < ω.length) :
    (lis ω)[j]'(by simp [h]) = cs.wordProd (List.take j ω) * s ω[j] * (cs.wordProd (List.take j ω))⁻¹ :=
  by
  rw [← List.getD_eq_getElem (lis ω) 1, getD_leftInvSeq]
  simp [h]

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