length_wordProd_le

Mathlib.GroupTheory.Coxeter.Length

URI: https://scilib.ai/kg/mathlib#CoxeterSystem.length_wordProd_le

English

The length of the word product π ω is at most the length of ω; i.e., ℓ(π ω) ≤ ω.length.

Русский

Длина произведения слова π ω не больше длины ω; то есть ℓ(π ω) ≤ ω.length.

LaTeX

$$$\ell(\pi \omega) \le |\omega|$$$

Lean4

theorem length_wordProd_le (ω : List B) : ℓ(π ω) ≤ ω.length :=
  Nat.find_min' (cs.exists_word_with_prod (π ω)) ⟨ω, by tauto⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru