leftInvSeq_concat — Mathlib

English

The left inversion sequence satisfies a concatenation rule: leftInvSeq(ω.concat i) equals leftInvSeq(ω) concatenated with (π ω) * (s_i) * (π ω)^{-1}.

Русский

Левая последовательность инверсий удовлетворяет правилу конкатенации: leftInvSeq(ω.concat i) = leftInvSeq(ω).concat((π ω) s_i (π ω)^{-1}).

LaTeX

$$$cs.leftInvSeq(\omega \concat i) = (cs.leftInvSeq \omega) .concat ((\pi \omega) \cdot (s i) \cdot (\pi \omega)^{-1})$$$

Lean4

theorem leftInvSeq_concat (ω : List B) (i : B) : lis(ω.concat i) = (lis ω).concat ((π ω) * (s i) * (π ω)⁻¹) := by
  simp [leftInvSeq_eq_reverse_rightInvSeq_reverse, rightInvSeq]

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