unique_continuousLinearMapOfBilin

Mathlib.Analysis.InnerProductSpace.Dual

URI: https://scilib.ai/kg/mathlib#InnerProductSpace.unique_continuousLinearMapOfBilin

← MathLib Explorer

English

If for every w the inner product ⟪f, w⟫ equals B v w, then f equals B♯ v.

Русский

Если для всех w выполняется ⟪f, w⟫ = B(v,w), то f = B♯ v.

LaTeX

$$(∀ w, ⟪f, w⟫ = B(v, w)) → f = B♯ v$$

Lean4

theorem unique_continuousLinearMapOfBilin {v f : E} (is_lax_milgram : ∀ w, ⟪f, w⟫ = B v w) : f = B♯ v :=
  by
  refine ext_inner_right 𝕜 ?_
  intro w
  rw [continuousLinearMapOfBilin_apply]
  exact is_lax_milgram w

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru