takeI_length — Mathlib

English

For any α with an inhabited instance, the length of takeI n l equals n for all n and l.

Русский

Для любых n и списка l имеем: длина takeI n l равна n при условии существования значения по умолчанию для типа α.

LaTeX

$$$\\mathrm{length}(\\mathrm{takeI}(n, l)) = n$$$

Lean4

@[simp]
theorem takeI_length : ∀ n l, length (@takeI α _ n l) = n
  | 0, _ => rfl
  | _ + 1, _ => congr_arg succ (takeI_length _ _)

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