mapDomain_comp — Mathlib

English

Transport along a composition of maps equals successive transports.

Русский

Перенос вдоль композиции функций равен последовательному переносу.

LaTeX

$$$\\operatorname{mapDomain}\\,(g \\circ f)\\, v = \\operatorname{mapDomain}\\, g\\, (\\operatorname{mapDomain}\\, f\\, v).$$$

Lean4

theorem mapDomain_comp {f : α → β} {g : β → γ} : mapDomain (g ∘ f) v = mapDomain g (mapDomain f v) :=
  by
  refine ((sum_sum_index ?_ ?_).trans ?_).symm
  · intro
    exact single_zero _
  · intro
    exact single_add _
  refine sum_congr fun _ _ => sum_single_index ?_
  exact single_zero _

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