list_map — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Function.LeftInverse.list_map {f : α → β} {g : β → α} (h : LeftInverse f g) : LeftInverse (map f) (map g)
  | [] => by simp_rw [map_nil]
  | x :: xs => by simp_rw [map_cons, h x, h.list_map xs]

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