`BookProof.ChapterSirkPerSystemFlowBound.norm_adjoint_apply_le_of_isometry` (V : G →L[ℂ] E) (hV : ∀ x : G, ‖V x‖ = ‖x‖) (v : E) : ‖V.adjoint v‖ ≤ ‖v‖

Initializing...

`BookProof.ChapterSirkPerSystemFlowBound.norm_adjoint_apply_le_of_isometry` (V : G →L[ℂ] E) (hV : ∀ x : G, ‖V x‖ = ‖x‖) (v : E) : ‖V.adjoint v‖ ≤ ‖v‖ · Prove2Me