take — Mathlib

English

If ω is reduced, then every initial segment take j ω is also reduced.

Русский

Если ω редуцировано, то каждая начальная префиксация take j ω тоже редуцирована.

LaTeX

$$$$ cs.IsReduced(\\\\omega) \\\\Rightarrow \\\\forall j, cs.IsReduced(\\\\omega.take(j)) $$$$

Lean4

theorem take {cs : CoxeterSystem M W} {ω : List B} (hω : cs.IsReduced ω) (j : ℕ) : cs.IsReduced (ω.take j) :=
  (isReduced_take_and_drop _ hω _).1

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