map_comp — Mathlib

English

Composing two injective affine maps and then applying the pushforward equals pushing forward by the composition of the maps in two steps.

Русский

Сведение по каскадному применению двух инъективных аффинных отображений эквивалентно применению композиции отображений в два шага.

LaTeX

$$$s.map(g \\circ f) (hg \\circ hf) = (s.map f hf).map g hg$$$

Lean4

theorem map_comp {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective f) (g : P₂ →ᵃ[k] P₃)
    (hg : Function.Injective g) : s.map (g.comp f) (hg.comp hf) = (s.map f hf).map g hg :=
  ext fun _ => rfl

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