proposition: Lemma contraction_cvg_fixed : closed U -> limn y = f (limn y).
proof: Proof. move=> clU; apply: cvg_lim => //. apply/cvgrPdist_lt => _/posnumP[e]; near_simpl; apply: near_inftyS. have [q_gt0 | | q0] := ltrgt0P q%:num. - near=> n => /=; apply: (le_lt_trans (@ctrfq (_, _) _)) => //=. + split; last exact: funS. by apply: closed_cvg contraction_cvg => //; apply: nearW => ?; exact: funS. + rewrite -ltr_pdivlMl //; near: n; move/cvgrPdist_lt: contraction_cvg. by apply; rewrite mulr_gt0 // invr_gt0. - by rewrite ltNge//; exact: contraNP. - apply: nearW => /= n; apply: (le_lt_trans (@ctrfq (_, _) _)). + split; last exact: funS. by apply: closed_cvg contraction_cvg => //; apply: nearW => ?; exact: funS. + by rewrite q0 mul0r. Unshelve. all: end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau