eq_adjoint_iff_basis_right — Mathlib

English

For a basis b of F, A: E→F, B: F→E, A = B† iff ∀ i x, ⟪A x, b_i⟫ = ⟪x, B(b_i)⟫.

Русский

Для базиса b пространства F, отображения A: E→F, B: F→E, A = B† тогда и только тогда, когда ∀ i и x выполняется ⟪A x, b_i⟫ = ⟪x, B(b_i)⟫.

LaTeX

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

Lean4

theorem eq_adjoint_iff_basis_right {ι : Type*} (b : Basis ι 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
    A = B.adjoint ↔ ∀ i x, ⟪A x, b i⟫ = ⟪x, B (b i)⟫ :=
  by
  refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
  ext x
  exact ext_inner_right_basis b fun i => by simp only [h i, adjoint_inner_left]

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