hasStrictFDerivAt_reApplyInnerSelf

English

If K is dense and ∀ v ∈ K, ⟪v,x⟫ = 0, then x = 0 (right-orthogonality version).

Русский

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

LaTeX

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

Lean4

theorem _root_.LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf {T : F →L[ℝ] F}
    (hT : (T : F →ₗ[ℝ] F).IsSymmetric) (x₀ : F) : HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ (T x₀))) x₀ :=
  by
  convert T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀) using 1
  ext y
  rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply, id, ContinuousLinearMap.id_apply, hT.apply_clm x₀ y,
    real_inner_comm _ x₀, two_smul]

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