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

Initializing...

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