mapsTo_prodMap_diagonal — Mathlib

English

If f maps the diagonal of α to the diagonal of β, then every pair (a,a) maps to (f a, f a).

Русский

Если отображение f переводит диагональ α в диагональ β, то каждый элемент на диагонали сохраняется как пара (f a, f a).

LaTeX

$$$ MapsTo\\ (Prod.map\\ f\\ f)\\ (diagonal\\ α)\\ (diagonal\\ β) $$$

Lean4

theorem mapsTo_prodMap_diagonal : MapsTo (Prod.map f f) (diagonal α) (diagonal β) :=
  diagonal_subset_iff.2 fun _ => rfl

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