# HG changeset patch # User hoelzl # Date 1396260997 -7200 # Node ID 9597a53b3429f39d56142e6db13af2548785522a # Parent b3551501424ea0ced6897336d51edd883065c08a add connected_local_const diff -r b3551501424e -r 9597a53b3429 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Mon Mar 31 12:16:35 2014 +0200 +++ b/src/HOL/Topological_Spaces.thy Mon Mar 31 12:16:37 2014 +0200 @@ -2134,8 +2134,37 @@ lemma connected_empty[simp]: "connected {}" by (auto intro!: connectedI) +lemma connectedD: + "connected A \ open U \ open V \ U \ V \ A = {} \ A \ U \ V \ U \ A = {} \ V \ A = {}" + by (auto simp: connected_def) + end +lemma connected_local_const: + assumes "connected A" "a \ A" "b \ A" + assumes *: "\a\A. eventually (\b. f a = f b) (at a within A)" + shows "f a = f b" +proof - + obtain S where S: "\a. a \ A \ a \ S a" "\a. a \ A \ open (S a)" + "\a x. a \ A \ x \ S a \ x \ A \ f a = f x" + using * unfolding eventually_at_topological by metis + + let ?P = "\b\{b\A. f a = f b}. S b" and ?N = "\b\{b\A. f a \ f b}. S b" + have "?P \ A = {} \ ?N \ A = {}" + using `connected A` S `a\A` + by (intro connectedD) (auto, metis) + then show "f a = f b" + proof + assume "?N \ A = {}" + then have "\x\A. f a = f x" + using S(1) by auto + with `b\A` show ?thesis by auto + next + assume "?P \ A = {}" then show ?thesis + using `a \ A` S(1)[of a] by auto + qed +qed + lemma (in linorder_topology) connectedD_interval: assumes "connected U" and xy: "x \ U" "y \ U" and "x \ z" "z \ y" shows "z \ U"