proposition: Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) : {for x, continuous f} -> (\forall y \near f x, P y) -> (\near x, P (f x)).
proof: Proof. exact. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed