unique_continuousLinearEquivOfBilin

English

The application of the continuous linear equivalence to a vector reproduces the bilinear form value.

Русский

Применение непрерывной линейной эквивалентности к вектору воспроизводит значение билинейной формы.

LaTeX

$$$ (coercive.continuousLinearEquivOfBilin v)(w) $ satisfies inner product relation with B.$$

Lean4

theorem unique_continuousLinearEquivOfBilin (coercive : IsCoercive B) {v f : V}
    (is_lax_milgram : ∀ w, ⟪f, w⟫_ℝ = B v w) : f = coercive.continuousLinearEquivOfBilin v :=
  unique_continuousLinearMapOfBilin B is_lax_milgram

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