isAdjointPair_inner — Mathlib

English

Equivalent adjoint relation expressed using a basis for E: A = B† iff ∀ i, y, ⟪A(b_i), y⟫ = ⟪b_i, B y⟫.

Русский

Эквивалентное отношение сопряжения через базис E: A = B† тогда и только тогда, когда ∀ i, y выполняется ⟪A(b_i), y⟫ = ⟪b_i, B y⟫.

LaTeX

$$$$A = B^{*} \iff \forall i,y, \langle A(b_i), y\rangle = \langle b_i, B y\rangle.$$$$

Lean4

theorem isAdjointPair_inner (A : E →ₗ[𝕜] F) :
    IsAdjointPair (sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜) (sesqFormOfInner : F →ₗ[𝕜] F →ₗ⋆[𝕜] 𝕜) A A.adjoint :=
  by
  intro x y
  simp only [sesqFormOfInner_apply_apply, adjoint_inner_left]

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