reverse — Mathlib

English

For every w in W, there exists a word ω such that ω is reduced and w equals the product π ω.

Русский

Для каждого w в W существует слово ω, которое редуцировано и удовлетворяет w = π ω.

LaTeX

$$$\\\\exists \\\\omega:[B], cs.IsReduced(\\\\omega) \\\\wedge w = cs.wordProd(\\\\omega)$$$

Lean4

theorem reverse {cs : CoxeterSystem M W} {ω : List B} (hω : cs.IsReduced ω) : cs.IsReduced (ω.reverse) :=
  (cs.isReduced_reverse_iff ω).mpr hω

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