`BookProof.ChapterResidualStream.norm_sub_residual_ge` {f : E → E} {L : ℝ} (hf : ∀ x y, ‖f x - f y‖ ≤ L * ‖x - y‖) (x y : E) : (1 - L) * ‖x - y‖ ≤ ‖residual f x

Initializing...

`BookProof.ChapterResidualStream.norm_sub_residual_ge` {f : E → E} {L : ℝ} (hf : ∀ x y, ‖f x - f y‖ ≤ L * ‖x - y‖) (x y : E) : (1 - L) * ‖x - y‖ ≤ ‖residual f x - residual... · Prove2Me