eq_of_inner_right

Mathlib.Analysis.InnerProductSpace.Projection.Submodule

URI: https://scilib.ai/kg/mathlib#Dense.eq_of_inner_right

← MathLib Explorer

English

If K is dense and ⟪v,x⟫ = 0 for all v ∈ K, then x = 0.

Русский

Если K плотное и для всех v∈K ⟪v,x⟫ = 0, то x = 0.

LaTeX

$$$\\text{Dense}(K) \\Rightarrow (\\forall v\\in K, ⟪v,x⟫ = 0) \\Rightarrow x=0$.$$

Lean4

theorem eq_of_inner_right (hK : Dense (K : Set E)) (h : ∀ v : K, ⟪(v : E), x⟫ = ⟪(v : E), y⟫) : x = y :=
  hK.eq_of_sub_mem_orthogonal (Submodule.sub_mem_orthogonal_of_inner_right h)

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

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

Разделы

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

Аффилиация

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