exists_reduced_word' — Mathlib

English

Same as previous item: there exists a reduced word representing w.

Русский

То же, что и ранее: существует редуцированное слово, представляющее w.

LaTeX

$$$\\\\exists \\\\omega: cs.IsReduced(\\\\omega) \\\\wedge w = cs.wordProd(\\\\omega)$$$

Lean4

theorem exists_reduced_word' (w : W) : ∃ ω : List B, cs.IsReduced ω ∧ w = π ω :=
  by
  rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
  use ω
  tauto

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