mapDomain_comp — Mathlib

English

Composition of mapDomain corresponds to composing the domain maps: mapDomain (g ∘ f) v equals mapDomain g (mapDomain f v).

Русский

Сложение областей через композицию: mapDomain (g ∘ f) v = mapDomain g (mapDomain f v).

LaTeX

$$$$ mapDomain (g \circ f) v = mapDomain g (mapDomain f v) $$$$

Lean4

theorem mapDomain_comp : mapDomain (g ∘ f) v = mapDomain g (mapDomain f v) :=
  ((sum_sum_index (single_zero <| g ·) (single_add <| g ·)).trans
      (sum_congr fun _ _ ↦ sum_single_index (single_zero _))).symm

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