theorem lipschitzWith_one_iff_residualMap_cocoerciveOn_half {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} (T : ↑D → H) : LipschitzWith 1 T ↔ CocoerciveOn (1 / 2) D (residualMap D T)

Proposition 4.11: a map on a subset of a real inner product space is nonexpansive exactly when its residual map Id - T is 1 / 2-cocoercive.