map_piSingle — Mathlib

English

Let X and Y be finite sets, and f: X → Y. For any x ∈ X and m ∈ M, applying the map induced on functions by f to the Pi-single function at x with value m yields the Pi-single function at f(x) with value m.

Русский

Пусть X и Y конечные множества, задано f: X → Y. Пусть x ∈ X и m ∈ M. Применение индуцированного отображения к функции с единственным значением m в x даёт функцию с единственным значением m в f(x).

LaTeX

$$$\operatorname{map} f (\Pi\text{single } x\, m) = \Pi\text{single } (f\,x)\, m$$$

Lean4

@[simp]
theorem map_piSingle [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) (m : M) :
    map f (Pi.single x m) = Pi.single (f x) m := by simp [map]

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