map — Mathlib

English

Let e be a diagonal element of Sym2 α. For any function f: α → β, e.map f is diagonal in Sym2 β.

Русский

Пусть e — диагональный элемент Sym2 α. Для любой функции f: α → β, e.map f диагонален в Sym2 β.

LaTeX

$$$$ \forall e \in \mathrm{Sym2}(\alpha), \forall f: \alpha \to \beta, \IsDiag(e) \to \IsDiag(e.map\,f). $$$$

Lean4

protected theorem map : e.IsDiag → (e.map f).IsDiag :=
  Sym2.ind (fun _ _ ↦ congr_arg f) e

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