lookup_graph — Mathlib

English

Let f: α → β. For any a and any as: List α, if a ∈ as, then lookup a (as.map (λ x, (x, f x))) = some (f a).

Русский

Пусть f: α → β. Пусть a и список as: List α. Если a ∈ as, то lookup a (as.map (λ x, (x, f x))) = some (f a).

LaTeX

$$$(a \\in as) \\rightarrow \\mathrm{lookup}\\; a\\; (\\mathrm{map}(\\lambda x.(x, f\\,x))\\; as) = \\text{Some}(f\\,a)$$$

Lean4

theorem lookup_graph (f : α → β) {a : α} {as : List α} (h : a ∈ as) :
    lookup a (as.map fun x => (x, f x)) = some (f a) := by induction as with grind

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