two_mul_semilength_eq_length — Mathlib

English

For every p, the length of its step list is twice its semilength.

Русский

Для каждого p длина списка шагов равна удвоенному семилength.

LaTeX

$$$$ 2 \cdot \operatorname{semilength}(p) = |p.toList|. $$$$

Lean4

@[simp]
theorem two_mul_semilength_eq_length : 2 * p.semilength = p.toList.length :=
  by
  nth_rw 1 [two_mul, semilength, p.count_U_eq_count_D, semilength]
  convert (p.toList.length_eq_countP_add_countP (· == D)).symm
  rw [count]; congr!; rename_i s; cases s <;> tauto

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