isSelfAdjoint — Mathlib

English

An indexed family f: ι → α_i is self-adjoint iff each coordinate f(i) is self-adjoint.

Русский

Элемент семейства f: ι → α_i сам-сопряжён тогда и только тогда, когда каждая координата f(i) самопряжена.

LaTeX

$$$\mathrm{IsSelfAdjoint}(f) \;\Leftrightarrow\; \forall i,\; \mathrm{IsSelfAdjoint}(f(i)).$$$

Lean4

protected theorem isSelfAdjoint : IsSelfAdjoint f ↔ ∀ i, IsSelfAdjoint (f i) :=
  funext_iff

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