isRightInversion_of_mem_rightInvSeq

English

If ω is reduced, then the sequence ris ω has no repeated elements.

Русский

Если ω сокращена, то ris ω не содержит повторяющихся элементов.

LaTeX

$$0$$

Lean4

theorem isRightInversion_of_mem_rightInvSeq {ω : List B} (hω : cs.IsReduced ω) {t : W} (ht : t ∈ ris ω) :
    cs.IsRightInversion (π ω) t := by
  constructor
  · exact cs.isReflection_of_mem_rightInvSeq ω ht
  · obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht
    rw [← List.getD_eq_getElem _ 1 hj, wordProd_mul_getD_rightInvSeq]
    rw [cs.length_rightInvSeq] at hj
    calc
      ℓ(π(ω.eraseIdx j))
      _ ≤ (ω.eraseIdx j).length := (cs.length_wordProd_le _)
      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
      _ = ℓ(π ω) := hω.symm

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