leftInvSeq_take — Mathlib

English

If a word’s right-inverse sequence contains an element, the corresponding reflection is in the group.

Русский

Если в правой инверсной последовательности слова содержится элемент, соответствующее отражение принадлежит группе.

LaTeX

$$$\\forall \\omega, \\; t \\in \\mathrm{ris}(\\omega) \\Rightarrow cs.IsReflection(t)$$$

Lean4

theorem leftInvSeq_take (ω : List B) (j : ℕ) : lis(ω.take j) = (lis ω).take j :=
  by
  simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse]
  rw [List.take_reverse]
  nth_rw 1 [← List.reverse_reverse ω]
  rw [List.take_reverse]
  simp [rightInvSeq_drop]

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