compAlternatingMap_apply — Mathlib

English

Applying the composed alternating map to an argument m yields the same result as applying f to m and then applying g.

Русский

Применение композиции чередующегося отображения к аргументу m даёт тот же результат, что и сначала применение f к m, затем применение g.

LaTeX

$$$ \big( g \circ_{\mathrm{Alt}} f \big)(m) = g\big( f(m) \big) $$$

Lean4

@[simp]
theorem compAlternatingMap_apply (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (m : ι → M) :
    g.compAlternatingMap f m = g (f m) :=
  rfl

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