theorem CoxeterBruhat.isReduced_tail {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (a : B) (rest : List B) (hred : cs.IsReduced (a :: rest)) : cs.IsReduced rest

The tail of a reduced word is reduced.

theorem CoxeterBruhat.isReduced_dropLast {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (hne : ω ≠ []) (hred : cs.IsReduced ω) : cs.IsReduced ω.dropLast

Dropping the last letter of a nonempty reduced word leaves a reduced word.

theorem CoxeterBruhat.isReduced_length_eq {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω₁ ω₂ : List B) (h1 : cs.IsReduced ω₁) (h2 : cs.IsReduced ω₂) (heq : cs.wordProd ω₁ = cs.wordProd ω₂) : ω₁.length = ω₂.length

Two reduced expressions for the same element have equal length.

theorem CoxeterBruhat.List.toFinset_sublist_subset {B : Type u_1} [DecidableEq B] [Fintype B] {l₁ l₂ : List B} (h : l₁.Sublist l₂) : l₁.toFinset ⊆ l₂.toFinset

A list sublist gives a subset on the underlying toFinset.

theorem CoxeterBruhat.toFinset_cover {B : Type u_1} [DecidableEq B] [Fintype B] (a b : B) (rest : List B) : (a :: b :: rest).toFinset ⊆ (b :: rest).toFinset ∪ (a :: b :: rest).dropLast.toFinset

The support of $a :: b :: \mathrm{rest}$ is covered by the supports of its tail and its dropLast.

theorem CoxeterBruhat.support_subset {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC_full : StrongExchangeCondition cs) (hRSP : ReducedSublistProperty cs) (hSEC : StrongExchangeForBruhat cs) {ω₁ ω₂ : List B} (hred₁ : cs.IsReduced ω₁) (hred₂ : cs.IsReduced ω₂) (heq : cs.wordProd ω₁ = cs.wordProd ω₂) : ω₁.toFinset ⊆ ω₂.toFinset

Support is well-defined: if $\omega_1, \omega_2$ are two reduced words for the same element, then $\operatorname{supp}(\omega_1) \subseteq \operatorname{supp}(\omega_2)$ — the set of simple generators appearing in a reduced expression depends only on the group element.