eq_adjoint_iff_basis_left — Mathlib

English

For a basis b and operators A: E→F, B: F→E, A = B† if and only if ∪ ∀ i, y, ⟪A(b_i), y⟫ = ⟪b_i, B y⟫.

Русский

Для базиса b и отображений A: E→F, B: F→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 eq_adjoint_iff_basis_left {ι : Type*} (b : Basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
    A = B.adjoint ↔ ∀ i y, ⟪A (b i), y⟫ = ⟪b i, B y⟫ :=
  by
  refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => Basis.ext b fun i => ?_⟩
  exact ext_inner_right 𝕜 fun y => by simp only [h i, adjoint_inner_left]

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