adjointAux_unique — Mathlib

English

If y ∈ T.adjointDomain and hx₀ satisfies ⟪x₀, x⟫ = ⟪y, T x⟫ for all x ∈ T.domain, then adjointAux hT y = x₀.

Русский

Если y ∈ T.adjointDomain и существует x₀ ∈ E, удовлетворяющее ⟪x₀, x⟫ = ⟪y, T x⟫ для всех x ∈ T.domain, то adjointAux hT y = x₀.

LaTeX

$$adjointAux hT y = x₀$$

Lean4

theorem adjointAux_unique (y : T.adjointDomain) {x₀ : E} (hx₀ : ∀ x : T.domain, ⟪x₀, x⟫ = ⟪(y : F), T x⟫) :
    adjointAux hT y = x₀ :=
  hT.eq_of_inner_left fun v => (adjointAux_inner hT _ _).trans (hx₀ v).symm

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