eq_zero_of_inner_left — Mathlib

English

If K is dense in E and x satisfies ⟪x,v⟫ = 0 for all v ∈ K (viewed inside K), then x must be the zero vector.

Русский

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

LaTeX

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

Lean4

theorem eq_zero_of_inner_left (hK : Dense (K : Set E)) (h : ∀ v : K, ⟪x, v⟫ = 0) : x = 0 :=
  by
  have : (⟪x, ·⟫) = 0 := (continuous_const.inner continuous_id).ext_on hK continuous_const (Subtype.forall.1 h)
  simpa using congr_fun this x

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