author nipkow Tue, 05 Nov 2019 14:57:41 +0100 changeset 71033 c1b63124245c parent 71032 acedd04c1a42 child 71039 ddd4aefc540f child 71040 9d2753406c60
tuned
```--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 13:56:34 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 14:57:41 2019 +0100
@@ -32,7 +32,7 @@
by (auto intro!: real_le_rsqrt)
qed

-subsection \<open>Continuity of the representation WRT an orthogonal basis\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity of the representation WRT an orthogonal basis\<close>

lemma orthogonal_Basis: "pairwise orthogonal Basis"
by (simp add: inner_not_same_Basis orthogonal_def pairwise_def)
@@ -353,8 +353,8 @@

subsection \<open>Boxes\<close>

-abbreviation One :: "'a::euclidean_space"
-  where "One \<equiv> \<Sum>Basis"
+abbreviation\<^marker>\<open>tag important\<close> One :: "'a::euclidean_space" where
+"One \<equiv> \<Sum>Basis"

lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
proof -
@@ -366,14 +366,14 @@
with independent_Basis show False by force
qed

-corollary One_neq_0[iff]: "One \<noteq> 0"
+corollary\<^marker>\<open>tag unimportant\<close> One_neq_0[iff]: "One \<noteq> 0"
by (metis One_non_0)

-corollary Zero_neq_One[iff]: "0 \<noteq> One"
+corollary\<^marker>\<open>tag unimportant\<close> Zero_neq_One[iff]: "0 \<noteq> One"
by (metis One_non_0)

-definition\<^marker>\<open>tag important\<close> (in euclidean_space) eucl_less (infix "<e" 50)
-  where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
+definition\<^marker>\<open>tag important\<close> (in euclidean_space) eucl_less (infix "<e" 50) where
+"eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"

definition\<^marker>\<open>tag important\<close> box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
definition\<^marker>\<open>tag important\<close> "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"```