adjointDomainMkCLM — Mathlib

English

The unique continuous extension of adjointDomainMkCLM to the whole ambient space E exists and is defined on each y ∈ T.adjointDomain.

Русский

Существует единственное непрерывное продолжение adjointDomainMkCLM на всю окружающую пространство E, определяемое на каждом y ∈ T.adjointDomain.

LaTeX

$$adjointDomainMkCLMExtend hT y : StrongDual 𝕜 E$$

Lean4

/-- The operator `fun x ↦ ⟪y, T x⟫` considered as a continuous linear operator
from `T.adjointDomain` to `𝕜`. -/
def adjointDomainMkCLM (y : T.adjointDomain) : StrongDual 𝕜 T.domain :=
  ⟨(innerₛₗ 𝕜 (y : F)).comp T.toFun, y.prop⟩

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