adjointDomainMkCLMExtend_apply — Mathlib

English

For y ∈ T.adjointDomain and x ∈ T.domain, adjointDomainMkCLMExtend hT y (x) = ⟪y, T x⟫.

Русский

Для y ∈ T.adjointDomain и x ∈ T.domain, adjointDomainMkCLMExtend hT y (x) = ⟪y, T x⟫.

LaTeX

$$adjointDomainMkCLMExtend hT y (x : E) = ⟪(y : F), T x⟫$$

Lean4

@[simp]
theorem adjointDomainMkCLMExtend_apply (y : T.adjointDomain) (x : T.domain) :
    adjointDomainMkCLMExtend hT y (x : E) = ⟪(y : F), T x⟫ :=
  ContinuousLinearMap.extend_eq _ _ _ _ _

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