continuousLinearEquivOfBilin — Mathlib

English

The evaluation identity holds at the level of inner products for the continuous linear equivalence corresponding to the bilinear form.

Русский

Тождество в применении к билинейной форме сохраняется на уровне внутренних произведений для соответствующей непрерывной линейной эквивалентности.

LaTeX

$$$ \langle \cdot, \cdot \rangle = \langle \cdot, \cdot \rangle \text{ under equivalence}. $$$

Lean4

/-- The Lax-Milgram equivalence of a coercive bounded bilinear operator:
for all `v : V`, `continuousLinearEquivOfBilin B v` is the unique element `V`
such that `continuousLinearEquivOfBilin B v, w⟫ = B v w`.
The Lax-Milgram theorem states that this is a continuous equivalence.
-/
def continuousLinearEquivOfBilin (coercive : IsCoercive B) : V ≃L[ℝ] V :=
  ContinuousLinearEquiv.ofBijective B♯ coercive.ker_eq_bot coercive.range_eq_top

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