length_lookmap — Mathlib

English

For any list l and any f : α → Option α, the operation lookmap preserves length: length(lookmap f l) = length l.

Русский

Для любого списка l и любого f : α → Option α операция lookmap сохраняет длину: длина(lookmap f l) = длина l.

LaTeX

$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\alpha\\ ,\\ \\mathrm{length}(\\mathrm{lookmap}\\ f\\ l) = \\mathrm{length}(l)$$$

Lean4

@[simp, grind =]
theorem length_lookmap (l : List α) : length (l.lookmap f) = length l := by
  rw [← length_map, lookmap_map_eq _ fun _ => (), length_map]; simp

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