--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Sep 29 12:58:55 2016 +0100
@@ -129,24 +129,28 @@
have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg")
proof (cases x c rule: le_cases)
case le show ?diff_fg
- apply (rule differentiable_transform_within [where d = "dist x c" and f = f])
- using x le st
- apply (simp_all add: dist_real_def)
- apply (rule differentiable_at_withinI)
- apply (rule differentiable_within_open [where s = "{a<..<c} - s", THEN iffD1], simp_all)
- apply (blast intro: open_greaterThanLessThan finite_imp_closed)
- apply (force elim!: differentiable_subset)+
- done
+ proof (rule differentiable_transform_within [where d = "dist x c" and f = f])
+ have "f differentiable at x within ({a<..<c} - s)"
+ apply (rule differentiable_at_withinI)
+ using x le st
+ by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost le st(3) x)
+ moreover have "open ({a<..<c} - s)"
+ by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
+ ultimately show "f differentiable at x within {a..b}"
+ using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+ qed (use x le st dist_real_def in auto)
next
case ge show ?diff_fg
- apply (rule differentiable_transform_within [where d = "dist x c" and f = g])
- using x ge st
- apply (simp_all add: dist_real_def)
- apply (rule differentiable_at_withinI)
- apply (rule differentiable_within_open [where s = "{c<..<b} - t", THEN iffD1], simp_all)
- apply (blast intro: open_greaterThanLessThan finite_imp_closed)
- apply (force elim!: differentiable_subset)+
- done
+ proof (rule differentiable_transform_within [where d = "dist x c" and f = g])
+ have "g differentiable at x within ({c<..<b} - t)"
+ apply (rule differentiable_at_withinI)
+ using x ge st
+ by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost)
+ moreover have "open ({c<..<b} - t)"
+ by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
+ ultimately show "g differentiable at x within {a..b}"
+ using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+ qed (use x ge st dist_real_def in auto)
qed
}
then have "\<exists>s. finite s \<and>
@@ -3801,7 +3805,7 @@
moreover have "{a<..<b} - k \<subseteq> {a..b} - k"
by force
ultimately have g_diff_at: "\<And>x. \<lbrakk>x \<notin> k; x \<in> {a<..<b}\<rbrakk> \<Longrightarrow> \<gamma> differentiable at x"
- by (metis Diff_iff differentiable_on_subset C1_diff_imp_diff [OF g_C1_diff] differentiable_on_def differentiable_within_open)
+ by (metis Diff_iff differentiable_on_subset C1_diff_imp_diff [OF g_C1_diff] differentiable_on_def at_within_open)
{ fix w
assume "w \<noteq> z"
have "continuous_on (ball w (cmod (w - z))) (\<lambda>w. 1 / (w - z))"
@@ -7527,4 +7531,32 @@
by (metis Cauchy_theorem_global assms winding_number_zero_in_outside valid_path_imp_path)
+lemma simply_connected_imp_winding_number_zero:
+ assumes "simply_connected s" "path g"
+ "path_image g \<subseteq> s" "pathfinish g = pathstart g" "z \<notin> s"
+ shows "winding_number g z = 0"
+proof -
+ have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z"
+ apply (rule winding_number_homotopic_paths)
+ apply (rule homotopic_loops_imp_homotopic_paths_null [where a = "pathstart g"])
+ apply (rule homotopic_loops_subset [of s])
+ using assms
+ apply (auto simp: homotopic_paths_imp_homotopic_loops path_defs simply_connected_eq_contractible_path)
+ done
+ also have "... = 0"
+ using assms by (force intro: winding_number_trivial)
+ finally show ?thesis .
+qed
+
+lemma Cauchy_theorem_simply_connected:
+ assumes "open s" "simply_connected s" "f holomorphic_on s" "valid_path g"
+ "path_image g \<subseteq> s" "pathfinish g = pathstart g"
+ shows "(f has_contour_integral 0) g"
+using assms
+apply (simp add: simply_connected_eq_contractible_path)
+apply (auto intro!: Cauchy_theorem_null_homotopic [where a = "pathstart g"]
+ homotopic_paths_imp_homotopic_loops)
+using valid_path_imp_path by blast
+
+
end
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Sep 29 12:58:55 2016 +0100
@@ -8697,6 +8697,59 @@
apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def)
by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)
+lemma rel_interior_convex_Int_affine:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}"
+ shows "rel_interior(S \<inter> T) = interior S \<inter> T"
+proof -
+ obtain a where aS: "a \<in> interior S" and aT:"a \<in> T"
+ using assms by force
+ have "rel_interior S = interior S"
+ by (metis (no_types) aS affine_hull_nonempty_interior equals0D rel_interior_interior)
+ then show ?thesis
+ by (metis (no_types) affine_imp_convex assms convex_rel_interior_inter_two hull_same rel_interior_affine_hull)
+qed
+
+lemma closure_convex_Int_affine:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" "affine T" "rel_interior S \<inter> T \<noteq> {}"
+ shows "closure(S \<inter> T) = closure S \<inter> T"
+proof
+ have "closure (S \<inter> T) \<subseteq> closure T"
+ by (simp add: closure_mono)
+ also have "... \<subseteq> T"
+ by (simp add: affine_closed assms)
+ finally show "closure(S \<inter> T) \<subseteq> closure S \<inter> T"
+ by (simp add: closure_mono)
+next
+ obtain a where "a \<in> rel_interior S" "a \<in> T"
+ using assms by auto
+ then have ssT: "subspace ((\<lambda>x. (-a)+x) ` T)" and "a \<in> S"
+ using affine_diffs_subspace rel_interior_subset assms by blast+
+ show "closure S \<inter> T \<subseteq> closure (S \<inter> T)"
+ proof
+ fix x assume "x \<in> closure S \<inter> T"
+ show "x \<in> closure (S \<inter> T)"
+ proof (cases "x = a")
+ case True
+ then show ?thesis
+ using \<open>a \<in> S\<close> \<open>a \<in> T\<close> closure_subset by fastforce
+ next
+ case False
+ then have "x \<in> closure(open_segment a x)"
+ by auto
+ then show ?thesis
+ using \<open>x \<in> closure S \<inter> T\<close> assms convex_affine_closure_Int by blast
+ qed
+ qed
+qed
+
+lemma rel_frontier_convex_Int_affine:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}"
+ shows "rel_frontier(S \<inter> T) = frontier S \<inter> T"
+by (simp add: assms convex_affine_rel_frontier_Int)
+
lemma subset_rel_interior_convex:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
--- a/src/HOL/Analysis/Derivative.thy Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Derivative.thy Thu Sep 29 12:58:55 2016 +0100
@@ -180,13 +180,6 @@
shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
-lemma differentiable_within_open: (* TODO: delete *)
- assumes "a \<in> s"
- and "open s"
- shows "f differentiable (at a within s) \<longleftrightarrow> f differentiable (at a)"
- using assms
- by (simp only: at_within_interior interior_open)
-
lemma differentiable_on_eq_differentiable_at:
"open s \<Longrightarrow> f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x)"
unfolding differentiable_on_def
@@ -207,6 +200,15 @@
lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S"
by (simp add: id_def)
+lemma differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. c) differentiable_on S"
+ by (simp add: differentiable_on_def)
+
+lemma differentiable_on_mult [simp, derivative_intros]:
+ fixes f :: "'M::real_normed_vector \<Rightarrow> 'a::real_normed_algebra"
+ shows "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) differentiable_on S"
+ apply (simp add: differentiable_on_def differentiable_def)
+ using differentiable_def differentiable_mult by blast
+
lemma differentiable_on_compose:
"\<lbrakk>g differentiable_on S; f differentiable_on (g ` S)\<rbrakk> \<Longrightarrow> (\<lambda>x. f (g x)) differentiable_on S"
by (simp add: differentiable_in_compose differentiable_on_def)
--- a/src/HOL/Analysis/Path_Connected.thy Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Sep 29 12:58:55 2016 +0100
@@ -2315,10 +2315,10 @@
"outside s \<inter> s = {}"
by (auto simp: outside_def)
-lemma inside_inter_outside [simp]: "inside s \<inter> outside s = {}"
+lemma inside_Int_outside [simp]: "inside s \<inter> outside s = {}"
by (auto simp: inside_def outside_def)
-lemma inside_union_outside [simp]: "inside s \<union> outside s = (- s)"
+lemma inside_Un_outside [simp]: "inside s \<union> outside s = (- s)"
by (auto simp: inside_def outside_def)
lemma inside_eq_outside:
@@ -2606,7 +2606,7 @@
by (simp add: inside_def connected_component_UNIV)
lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)"
-using inside_empty inside_union_outside by blast
+using inside_empty inside_Un_outside by blast
lemma inside_same_component:
"\<lbrakk>connected_component (- s) x y; x \<in> inside s\<rbrakk> \<Longrightarrow> y \<in> inside s"
@@ -2666,7 +2666,7 @@
fixes s :: "'a :: {real_normed_vector, perfect_space} set"
assumes "convex s"
shows "outside s = - s"
- by (metis ComplD assms convex_in_outside equalityI inside_union_outside subsetI sup.cobounded2)
+ by (metis ComplD assms convex_in_outside equalityI inside_Un_outside subsetI sup.cobounded2)
lemma inside_convex:
fixes s :: "'a :: {real_normed_vector, perfect_space} set"
@@ -2761,7 +2761,7 @@
have "closure (inside s) \<inter> - inside s = closure (inside s) - interior (inside s)"
by (metis (no_types) Diff_Compl assms closure_closed interior_closure open_closed open_inside)
moreover have "- inside s \<inter> - outside s = s"
- by (metis (no_types) compl_sup double_compl inside_union_outside)
+ by (metis (no_types) compl_sup double_compl inside_Un_outside)
moreover have "closure (inside s) \<subseteq> - outside s"
by (metis (no_types) assms closure_inside_subset union_with_inside)
ultimately have "closure (inside s) - interior (inside s) \<subseteq> s"
@@ -5460,21 +5460,6 @@
subsection\<open>Components, continuity, openin, closedin\<close>
-lemma continuous_openin_preimage_eq:
- "continuous_on S f \<longleftrightarrow>
- (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
-apply (auto simp: continuous_openin_preimage_gen)
-apply (fastforce simp add: continuous_on_open openin_open)
-done
-
-lemma continuous_closedin_preimage_eq:
- "continuous_on S f \<longleftrightarrow>
- (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
-apply safe
-apply (simp add: continuous_closedin_preimage)
-apply (fastforce simp add: continuous_on_closed closedin_closed)
-done
-
lemma continuous_on_components_gen:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
assumes "\<And>c. c \<in> components S \<Longrightarrow>
@@ -6108,7 +6093,6 @@
apply (metis assms homotopy_eqv_homotopic_triviality_imp)
by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym)
-
lemma homotopy_eqv_cohomotopic_triviality_null_imp:
fixes S :: "'a::real_normed_vector set"
and T :: "'b::real_normed_vector set"
@@ -6156,7 +6140,6 @@
apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp)
by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym)
-
lemma homotopy_eqv_contractible_sets:
fixes S :: "'a::real_normed_vector set"
and T :: "'b::real_normed_vector set"
@@ -6215,6 +6198,50 @@
lemma homeomorphic_contractible:
fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
-by (metis homeomorphic_contractible_eq)
+ by (metis homeomorphic_contractible_eq)
+
+subsection\<open>Misc other results\<close>
+
+lemma bounded_connected_Compl_real:
+ fixes S :: "real set"
+ assumes "bounded S" and conn: "connected(- S)"
+ shows "S = {}"
+proof -
+ obtain a b where "S \<subseteq> box a b"
+ by (meson assms bounded_subset_open_interval)
+ then have "a \<notin> S" "b \<notin> S"
+ by auto
+ then have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> - S"
+ by (meson Compl_iff conn connected_iff_interval)
+ then show ?thesis
+ using \<open>S \<subseteq> box a b\<close> by auto
+qed
+
+lemma bounded_connected_Compl_1:
+ fixes S :: "'a::{euclidean_space} set"
+ assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1"
+ shows "S = {}"
+proof -
+ have "DIM('a) = DIM(real)"
+ by (simp add: "1")
+ then obtain f::"'a \<Rightarrow> real" and g
+ where "linear f" "\<And>x. norm(f x) = norm x" "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
+ by (rule isomorphisms_UNIV_UNIV) blast
+ with \<open>bounded S\<close> have "bounded (f ` S)"
+ using bounded_linear_image linear_linear by blast
+ have "connected (f ` (-S))"
+ using connected_linear_image assms \<open>linear f\<close> by blast
+ moreover have "f ` (-S) = - (f ` S)"
+ apply (rule bij_image_Compl_eq)
+ apply (auto simp: bij_def)
+ apply (metis \<open>\<And>x. g (f x) = x\<close> injI)
+ by (metis UNIV_I \<open>\<And>y. f (g y) = y\<close> image_iff)
+ finally have "connected (- (f ` S))"
+ by simp
+ then have "f ` S = {}"
+ using \<open>bounded (f ` S)\<close> bounded_connected_Compl_real by blast
+ then show ?thesis
+ by blast
+qed
end
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Sep 29 12:58:55 2016 +0100
@@ -550,6 +550,11 @@
lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
by auto
+lemma closedin_Union:
+ assumes "finite S" "\<And>T. T \<in> S \<Longrightarrow> closedin U T"
+ shows "closedin U (\<Union>S)"
+ using assms by induction auto
+
lemma closedin_Inter[intro]:
assumes Ke: "K \<noteq> {}"
and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S"
@@ -6164,6 +6169,22 @@
using * by auto
qed
+lemma continuous_openin_preimage_eq:
+ "continuous_on S f \<longleftrightarrow>
+ (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply safe
+apply (simp add: continuous_openin_preimage_gen)
+apply (fastforce simp add: continuous_on_open openin_open)
+done
+
+lemma continuous_closedin_preimage_eq:
+ "continuous_on S f \<longleftrightarrow>
+ (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply safe
+apply (simp add: continuous_closedin_preimage)
+apply (fastforce simp add: continuous_on_closed closedin_closed)
+done
+
lemma continuous_open_preimage:
assumes "continuous_on s f"
and "open s"
@@ -9893,6 +9914,101 @@
by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
qed
+subsection\<open>Pasting functions together\<close>
+
+subsubsection\<open>on open sets\<close>
+
+lemma pasting_lemma:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+ shows "continuous_on S g"
+proof (clarsimp simp: continuous_openin_preimage_eq)
+ fix U :: "'b set"
+ assume "open U"
+ have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+ using clo openin_imp_subset by blast
+ have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
+ apply (auto simp: dest: S)
+ apply (metis (no_types, lifting) g mem_Collect_eq)
+ using clo f g openin_imp_subset by fastforce
+ show "openin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+ apply (subst *)
+ apply (rule openin_Union, clarify)
+ apply (metis (full_types) \<open>open U\<close> cont clo openin_trans continuous_openin_preimage_gen)
+ done
+qed
+
+lemma pasting_lemma_exists:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+ and clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+ show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+ apply (rule pasting_lemma [OF clo cont])
+ apply (blast intro: f)+
+ apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+ done
+next
+ fix x i
+ assume "i \<in> I" "x \<in> S \<inter> T i"
+ then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+ by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
+subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
+
+lemma pasting_lemma_closed:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes "finite I"
+ and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+ shows "continuous_on S g"
+proof (clarsimp simp: continuous_closedin_preimage_eq)
+ fix U :: "'b set"
+ assume "closed U"
+ have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
+ apply auto
+ apply (metis (no_types, lifting) g mem_Collect_eq)
+ using clo closedin_closed apply blast
+ apply (metis Int_iff f g clo closedin_limpt inf.absorb_iff2)
+ done
+ show "closedin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+ apply (subst *)
+ apply (rule closedin_Union)
+ using \<open>finite I\<close> apply simp
+ apply (blast intro: \<open>closed U\<close> continuous_closedin_preimage cont clo closedin_trans)
+ done
+qed
+
+lemma pasting_lemma_exists_closed:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes "finite I"
+ and S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+ and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+ show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+ apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
+ apply (blast intro: f)+
+ apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+ done
+next
+ fix x i
+ assume "i \<in> I" "x \<in> S \<inter> T i"
+ then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+ by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
no_notation
eucl_less (infix "<e" 50)