list_map — Mathlib

English

If h is RightInverse f g, then map f and map g are RightInverse as functions on lists.

Русский

Если h = RightInverse f g, то List.map f и List.map g образуют правый обратный пары на списках.

LaTeX

$$$\\\\forall {f:\\\\alpha \\\\to \\\\beta} {g:\\\\beta \\\\to \\\\alpha},\\\\,\\\\text{RightInverse } f g \\\\Rightarrow \\\\text{RightInverse } (\\\\operatorname{List.map} f) (\\\\operatorname{List.map} g).$$$

Lean4

nonrec theorem _root_.Function.RightInverse.list_map {f : α → β} {g : β → α} (h : RightInverse f g) :
    RightInverse (map f) (map g) :=
  h.list_map

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