continuousLinearEquivOfBilin_apply

English

If a coercive bilinear operator yields a unique bilinear mapping corresponding to given inner products, then the induced continuous linear equivalence is the unique such map.

Русский

Если коэрцитивная билинейная форма задаёт уникальное отображение, соответствующее внутреннему произведению, то полученная непрерывная линейная эквивалентность уникальна.

LaTeX

$$$ \text{If } \forall w, \langle f, w \rangle = B(v,w) \Rightarrow f = B \text{-equiv}(v),$$$

Lean4

@[simp]
theorem continuousLinearEquivOfBilin_apply (coercive : IsCoercive B) (v w : V) :
    ⟪coercive.continuousLinearEquivOfBilin v, w⟫_ℝ = B v w :=
  continuousLinearMapOfBilin_apply B v w

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