getD_map — Mathlib

English

Applying a function f to a list and then taking getD is the same as taking getD first and then applying f to the result.

Русский

Применение функции f к списку и затем получение getD эквивалентно сначала получению getD, а затем применению f к результату.

LaTeX

$$$$ (\\mathrm{map}\\ f\\ l).getD\\ n\\ (f\\ d) = f\\ (l.getD\\ n\\ d). $$$$

Lean4

theorem getD_map {n : ℕ} (f : α → β) : (map f l).getD n (f d) = f (l.getD n d) := by simp

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