map_map — Mathlib

English

Applying two maps g and f in succession is the same as applying g ∘ f once.

Русский

Применение двух отображений g и f последовательно эквивалентно применению g ∘ f один раз.

LaTeX

$$$\\mathrm{Sym.map}(g)(\\mathrm{Sym.map}(f)(s)) = \\mathrm{Sym.map}(g \\circ f)(s).$$$

Lean4

@[simp]
theorem map_map {α β γ : Type*} {n : ℕ} (g : β → γ) (f : α → β) (s : Sym α n) :
    Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s :=
  Subtype.ext <| by dsimp only [Sym.map]; simp

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