prodMap — Mathlib

English

Let f: α → α and g: β → β. If a is fixed by f and b is fixed by g, then (a, b) is fixed by the product map Prod.map f g; i.e., (a, b) is unchanged under applying f to the first coordinate and g to the second.

Русский

Пусть f: α → α и g: β → β. Если a фиксирована f (f(a) = a) и b фиксирована g (g(b) = b), то пара (a, b) фиксирована отображением Prod.map f g, то есть (a, b) переходит в (a, b).

LaTeX

$$$ (f(a) = a) \land (g(b) = b) \\Rightarrow (f(a), g(b)) = (a, b) $$$

Lean4

theorem prodMap (ha : IsFixedPt f a) (hb : IsFixedPt g b) : IsFixedPt (Prod.map f g) (a, b) :=
  (isFixedPt_prodMap _).mpr ⟨ha, hb⟩

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