map_apply_ιMulti_family — Mathlib

English

For any I with a linear order, v:I→M, f:M→N, the equality (map n f) (ιMulti_family R n v s) = ιMulti_family R n (f∘v) s holds for any s with a card constraint.

Русский

Пусть I упорядочено, v:I→M, f:M→N. Тогда (map n f)(ιMulti_family R n v s) = ιMulti_family R n (f∘v) s при любом s с заданной длиной.

LaTeX

$$$ (map n f) (ιMulti\\_family R n v s) = ιMulti\\_family R n (f \\circ v) s $$$

Lean4

@[simp]
theorem map_apply_ιMulti_family {I : Type*} [LinearOrder I] (v : I → M) (f : M →ₗ[R] N)
    (s : { s : Finset I // s.card = n }) : (map n f) (ιMulti_family R n v s) = ιMulti_family R n (f ∘ v) s :=
  by
  simp only [ιMulti_family, map, alternatingMapLinearEquiv_apply_ιMulti]
  rfl

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