(N : D →ₗ[ℂ] D) (v : D) (hpos : 0 ≤ (inner ℂ ((N v : D) : F) ((v : F)) : ℂ).re) : ‖((N v : D) : F)‖ ≤ ‖((((N + LinearMap.id : D →ₗ[ℂ] D)) v : D) : F)‖

Initializing...

(N : D →ₗ[ℂ] D) (v : D) (hpos : 0 ≤ (inner ℂ ((N v : D) : F) ((v : F)) : ℂ).re) : ‖((N v : D) : F)‖ ≤ ‖((((N + LinearMap.id : D →ₗ[ℂ] D)) v : D) : F)‖ · Prove2Me