theorem quasinonexpansive_iterates_fejer_monotone {H : Type u} [NormedAddCommGroup H] {D : Set H} (T : ↑D → ↑D) (hT : IsQuasinonexpansiveOn fun (x : ↑D) => ↑(T x)) (x₀ : ↑D) : FejerMonotone (Subtype.val '' Function.fixedPoints T) fun (n : ℕ) => ↑(T^[n] x₀)

Example 5.3.2: the Picard iterates of a quasinonexpansive self-map are Fejér monotone with respect to the ambient realization of its fixed-point set.