proposition: Theorem banach_fixed_point : closed U -> U !=set0 -> exists2 p, U p & p = f p.
proof: Proof. case: ctrf => [q ctrq] ? [base Ubase]; exists (lim (iter n f base @[n -->\oo])). apply: closed_cvg (contraction_cvg ctrq Ubase) => //. by apply: nearW => ?; exact: funS. exact: (contraction_cvg_fixed ctrq). 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