Symmetric operators: negation and limits

Two facts about symmetric operators complementing Mathlib's Mathlib.Analysis.InnerProductSpace.Symmetric:

• the negative of a symmetric linear map is symmetric (LinearMap.IsSymmetric.neg);
• the symmetric bounded operators form a closed subset of E →L[𝕜] E (ContinuousLinearMap.isClosed_setOf_isSymmetric), so a limit of symmetric bounded operators is symmetric. No completeness of E is needed: the condition ⟪T x, y⟫ = ⟪x, T y⟫ is closed in T for each pair x, y.

theorem LinearMap.IsSymmetric.neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : (-T).IsSymmetric

The negative of a symmetric linear map is symmetric.

theorem ContinuousLinearMap.isClosed_setOf_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : IsClosed {T : E →L[𝕜] E | (↑T).IsSymmetric}

The symmetric bounded operators form a closed subset of E →L[𝕜] E.