(T : F →L[ℂ] F) (hT : IsSelfAdjoint T) (c : ℝ) : (∀ x : F, c * ‖x‖ ^ 2 ≤ (inner ℂ x (T x) : ℂ).re) ↔ ∀ μ ∈ spectrum ℝ T, c ≤ μ

Initializing...

(T : F →L[ℂ] F) (hT : IsSelfAdjoint T) (c : ℝ) : (∀ x : F, c * ‖x‖ ^ 2 ≤ (inner ℂ x (T x) : ℂ).re) ↔ ∀ μ ∈ spectrum ℝ T, c ≤ μ · Prove2Me