dlookup_isSome — Mathlib

English

For any a, l, the map of dlookup by the sigma-map equals the find? of the list by the predicate a = s.1.

Русский

Для любого a, l отображение dlookup через Sigma.map эквивалентно find? списка по предикату a = s.1.

LaTeX

$$$ (dlookup a l).map (\\Sigma.mk a) = \\mathrm{find?}(\\lambda s. a = s.1)\\ l $$$

Lean4

@[grind =]
theorem dlookup_isSome {a : α} {l : List (Sigma β)} : (dlookup a l).isSome ↔ a ∈ l.keys := by
  induction l with
  | nil => simp
  | cons s _ _ => by_cases a = s.fst <;> grind

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