theorem averaged_strictlyQuasinonexpansiveOn {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} {T : H → H} {α : ℝ} (hT : AveragedWith α fun (x : ↑D) => T ↑x) : StrictlyQuasinonexpansiveOn D T

Remark 4.36: an averaged self-map on D is strictly quasinonexpansive on D.

theorem averaged_quasinonexpansiveOn {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} {T : H → H} {α : ℝ} (hT : AveragedWith α fun (x : ↑D) => T ↑x) : QuasinonexpansiveOn D T

An averaged self-map on D is quasinonexpansive on D.