English
If g : β → γ and f : α → β, then mapping by f followed by g is the same as mapping by g ∘ f. Formally, Sym2.map g (Sym2.map f x) = Sym2.map (g ∘ f) x for all x ∈ Sym2 α.
Русский
Пусть g: β → γ и f: α → β. Тогда применение двух картировок последовательно эквивалентно применению композиции: Sym2.map g (Sym2.map f x) = Sym2.map (g ∘ f) x.
LaTeX
$$$ \\operatorname{Sym2.map} \\, g \\, (\\operatorname{Sym2.map} \\, f \\, x) = \\operatorname{Sym2.map} \\, (g \\circ f) \\, x. $$$
Lean4
theorem map_map {g : β → γ} {f : α → β} (x : Sym2 α) : map g (map f x) = map (g ∘ f) x := by induction x; aesop
