selfAdjointPart_apply — Mathlib

English

For a self-adjoint x, the self-adjoint part equals the element paired with its proof of self-adjointness: selfAdjointPart(x) = ⟨x, hx⟩.

Русский

Для самосопряжённого x самосопряжённая часть равна паре (x, hx) внутри соответствующего типа.

LaTeX

$$$\text{selfAdjointPart}(x) = \langle x, hx \rangle$$$

Lean4

theorem selfAdjointPart_apply {x : A} (hx : IsSelfAdjoint x) : selfAdjointPart R x = ⟨x, hx⟩ :=
  Subtype.eq (hx.coe_selfAdjointPart_apply R)

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