3778 assumes "connected s" "open s" "finite k" "continuous_on s f" "c \<in> s" "f c = y" |
3777 assumes "connected s" "open s" "finite k" "continuous_on s f" "c \<in> s" "f c = y" |
3779 "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x\<in>s" |
3778 "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x\<in>s" |
3780 shows "f x = y" |
3779 shows "f x = y" |
3781 proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s" |
3780 proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s" |
3782 apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer |
3781 apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer |
3783 apply(rule continuous_closed_in_preimage[OF assms(4) closed_sing]) |
3782 apply(rule continuous_closed_in_preimage[OF assms(4) closed_singleton]) |
3784 apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball |
3783 apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball |
3785 proof safe fix x assume "x\<in>s" |
3784 proof safe fix x assume "x\<in>s" |
3786 from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this] |
3785 from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this] |
3787 show "\<exists>e>0. ball x e \<subseteq> {xa \<in> s. f xa \<in> {f x}}" apply(rule,rule,rule e) |
3786 show "\<exists>e>0. ball x e \<subseteq> {xa \<in> s. f xa \<in> {f x}}" apply(rule,rule,rule e) |
3788 proof safe fix y assume y:"y \<in> ball x e" thus "y\<in>s" using e by auto |
3787 proof safe fix y assume y:"y \<in> ball x e" thus "y\<in>s" using e by auto |