isDiag_map — Mathlib

English

If f is injective, then e.map f is diagonal exactly when e is diagonal. Specifically, (e.map f).IsDiag ↔ e.IsDiag.

Русский

Если f инъективно, то диагональность сохраняется и обратно эквивалентна: (e.map f).IsDiag ↔ e.IsDiag.

LaTeX

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

Lean4

theorem isDiag_map (hf : Injective f) : (e.map f).IsDiag ↔ e.IsDiag :=
  Sym2.ind (fun _ _ ↦ hf.eq_iff) e

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