lookmap_cons — Mathlib

English

The lookmap of a cons cell equals a case analysis on f a: if f a = none, then a :: l.lookmap f; if f a = some b, then b :: l.

Русский

Lookmap конc элемента задаёт разбор по f a: если f a = none, то a :: l.lookmap f; если f a = some b, то b :: l.

LaTeX

$$$(a :: l).lookmap f = \\begin{cases} a :: l.lookmap f, & f a = none \\\\ b :: l, & f a = \\text{some } b \\end{cases}$$$

Lean4

@[grind =]
theorem lookmap_cons {a : α} {l : List α} :
    (a :: l).lookmap f =
      match f a with
      | none => a :: l.lookmap f
      | some b => b :: l :=
  by cases h : f a <;> simp_all

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