proposition: Lemma derivable_within_continuous f (i : interval R) : {in i, forall x, derivable f x 1} -> {within [set` i], continuous f}.
proof: Proof. move=> di; apply/continuous_in_subspaceT => z /[1!inE] zA. apply/differentiable_continuous; rewrite -derivable1_diffP. by apply: di; rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms