map_congr — Mathlib

English

If f and g agree on every element of s, then map f s = map g s.

Русский

Если f и g согласны на каждом элементе s, то map f s = map g s.

LaTeX

$$$\\forall f,g : \\alpha \\to \\beta,\\ (\\forall x \\in s, f(x)=g(x)) \\Rightarrow \\mathrm{Sym.map}(f)(s) = \\mathrm{Sym.map}(g)(s).$$$

Lean4

@[congr]
theorem map_congr {f g : α → β} {s : Sym α n} (h : ∀ x ∈ s, f x = g x) : map f s = map g s :=
  Subtype.ext <| Multiset.map_congr rfl h

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