`BookProof.FriedrichsCanonical.isSemibounded_of_isPositive_shift` {Dom : Submodule ℂ F} (H : D →ₗ[ℂ] F) (c : ℝ) (A : Dom →ₗ[ℂ] F) (hA : IsPositiveSelfAdjointExtension (H + (c : ℂ)

Initializing...

`BookProof.FriedrichsCanonical.isSemibounded_of_isPositive_shift` {Dom : Submodule ℂ F} (H : D →ₗ[ℂ] F) (c : ℝ) (A : Dom →ₗ[ℂ] F) (hA : IsPositiveSelfAdjointExtension (H + (c : ℂ) · Prove2Me