isLeftInversion_of_mem_leftInvSeq

English

If ω is reduced, then lis ω has no repeated elements.

Русский

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

LaTeX

$$0$$

Lean4

theorem isLeftInversion_of_mem_leftInvSeq {ω : List B} (hω : cs.IsReduced ω) {t : W} (ht : t ∈ lis ω) :
    cs.IsLeftInversion (π ω) t := by
  constructor
  · exact cs.isReflection_of_mem_leftInvSeq ω ht
  · obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht
    rw [← List.getD_eq_getElem _ 1 hj, getD_leftInvSeq_mul_wordProd]
    rw [cs.length_leftInvSeq] 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

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