# HG changeset patch # User huffman # Date 1244871037 25200 # Node ID 61ee6256d863254f510c3e5a4daa6920ab667c84 # Parent c8c96efa448834c66d1a8b1c5cad1b62b410edad generalize lemmas about inner diff -r c8c96efa4488 -r 61ee6256d863 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 12 22:20:36 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 12 22:30:37 2009 -0700 @@ -5169,12 +5169,11 @@ by auto lemma continuous_on_inner: - fixes s :: "(real ^ _) set" + fixes s :: "'a::real_inner set" shows "continuous_on s (inner a)" unfolding continuous_on by (rule ballI) (intro tendsto_intros) -lemma closed_halfspace_le: fixes a::"real^'n::finite" - shows "closed {x. inner a x \ b}" +lemma closed_halfspace_le: "closed {x. inner a x \ b}" proof- have *:"{x \ UNIV. inner a x \ {r. \x. inner a x = r \ r \ b}} = {x. inner a x \ b}" by auto let ?T = "{..b}" @@ -5188,10 +5187,10 @@ thus ?thesis unfolding closed_closedin[THEN sym] and * by auto qed -lemma closed_halfspace_ge: "closed {x::real^_. inner a x \ b}" +lemma closed_halfspace_ge: "closed {x. inner a x \ b}" using closed_halfspace_le[of "-a" "-b"] unfolding inner_minus_left by auto -lemma closed_hyperplane: "closed {x::real^_. inner a x = b}" +lemma closed_hyperplane: "closed {x. inner a x = b}" proof- have "{x. inner a x = b} = {x. inner a x \ b} \ {x. inner a x \ b}" by auto thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto @@ -5207,13 +5206,13 @@ text{* Openness of halfspaces. *} -lemma open_halfspace_lt: "open {x::real^_. inner a x < b}" +lemma open_halfspace_lt: "open {x. inner a x < b}" proof- have "UNIV - {x. b \ inner a x} = {x. inner a x < b}" by auto thus ?thesis using closed_halfspace_ge[unfolded closed_def Compl_eq_Diff_UNIV, of b a] by auto qed -lemma open_halfspace_gt: "open {x::real^_. inner a x > b}" +lemma open_halfspace_gt: "open {x. inner a x > b}" proof- have "UNIV - {x. b \ inner a x} = {x. inner a x > b}" by auto thus ?thesis using closed_halfspace_le[unfolded closed_def Compl_eq_Diff_UNIV, of a b] by auto @@ -5297,13 +5296,13 @@ text{* Some more convenient intermediate-value theorem formulations. *} -lemma connected_ivt_hyperplane: fixes y :: "real^'n::finite" +lemma connected_ivt_hyperplane: assumes "connected s" "x \ s" "y \ s" "inner a x \ b" "b \ inner a y" shows "\z \ s. inner a z = b" proof(rule ccontr) assume as:"\ (\z\s. inner a z = b)" - let ?A = "{x::real^'n. inner a x < b}" - let ?B = "{x::real^'n. inner a x > b}" + let ?A = "{x. inner a x < b}" + let ?B = "{x. inner a x > b}" have "open ?A" "open ?B" using open_halfspace_lt and open_halfspace_gt by auto moreover have "?A \ ?B = {}" by auto moreover have "s \ ?A \ ?B" using as by auto