src/HOL/Analysis/Starlike.thy

 
 section \<open>Line Segments\<close>
 
 subsection \<open>Midpoint\<close>
 
-definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
+definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
   where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
 
 lemma midpoint_idem [simp]: "midpoint x x = x"
   unfolding midpoint_def  by simp
 

 by (simp add: linear_iff midpoint_def)
 
 
 subsection \<open>Line segments\<close>
 
-definition%important closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
+definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
 
-definition%important open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
+definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   "open_segment a b \<equiv> closed_segment a b - {a,b}"
 
 lemmas segment = open_segment_def closed_segment_def
 
 lemma in_segment:

   by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
 
 
 subsection\<open>Starlike sets\<close>
 
-definition%important "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
 
 lemma starlike_UNIV [simp]: "starlike UNIV"
   by (simp add: starlike_def)
 
 lemma convex_imp_starlike:

   qed
   show "?rhs \<subseteq> ?lhs"
     by (meson hull_mono inf_mono subset_insertI subset_refl)
 qed
 
-subsection%unimportant\<open>More results about segments\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>More results about segments\<close>
 
 lemma dist_half_times2:
   fixes a :: "'a :: real_normed_vector"
   shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
 proof -

 lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
 
 
 subsection\<open>Betweenness\<close>
 
-definition%important "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
+definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
 
 lemma betweenI:
   assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
   shows "between (a, b) x"
 using assms unfolding between_def closed_segment_def by auto

   fixes x::real
   shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
   by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
 
 
-subsection%unimportant \<open>Shrinking towards the interior of a convex set\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>
 
 lemma mem_interior_convex_shrink:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S"
     and "c \<in> interior S"

   finally show ?thesis
     by (simp add: closure_mono dual_order.antisym)
 qed
 
 
-subsection%unimportant \<open>Some obvious but surprisingly hard simplex lemmas\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Some obvious but surprisingly hard simplex lemmas\<close>
 
 lemma simplex:
   assumes "finite S"
     and "0 \<notin> S"
   shows "convex hull (insert 0 S) = {y. \<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S \<le> 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}"

       using \<open>i \<notin> D\<close> unfolding span_substd_basis[OF assms(2)] using \<open>i \<in> Basis\<close> by auto
   qed
 qed
 
 
-subsection%unimportant \<open>Relative interior of convex set\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior of convex set\<close>
 
 lemma rel_interior_convex_nonempty_aux:
   fixes S :: "'n::euclidean_space set"
   assumes "convex S"
     and "0 \<in> S"

     done
 qed
 
 subsection\<open>The relative frontier of a set\<close>
 
-definition%important "rel_frontier S = closure S - rel_interior S"
+definition\<^marker>\<open>tag important\<close> "rel_frontier S = closure S - rel_interior S"
 
 lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
   by (simp add: rel_frontier_def)
 
 lemma rel_frontier_eq_empty:

   }
   ultimately show ?thesis by auto
 qed
 
 
-subsubsection%unimportant \<open>Relative interior and closure under common operations\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior and closure under common operations\<close>
 
 lemma rel_interior_inter_aux: "\<Inter>{rel_interior S |S. S \<in> I} \<subseteq> \<Inter>I"
 proof -
   {
     fix y

     and "convex T"
   shows "rel_frontier S \<times> rel_frontier T \<subseteq> rel_frontier (S \<times> T)"
     by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)
 
 
-subsubsection%unimportant \<open>Relative interior of convex cone\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior of convex cone\<close>
 
 lemma cone_rel_interior:
   fixes S :: "'m::euclidean_space set"
   assumes "cone S"
   shows "cone ({0} \<union> rel_interior S)"

   }
   then show "?lhs \<supseteq> ?rhs" by blast
 qed
 
 
-subsection%unimportant \<open>Convexity on direct sums\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity on direct sums\<close>
 
 lemma closure_sum:
   fixes S T :: "'a::real_normed_vector set"
   shows "closure S + closure T \<subseteq> closure (S + T)"
   unfolding set_plus_image closure_Times [symmetric] split_def

   qed
   then show ?thesis
     using \<open>y < x\<close> by (simp add: field_simps)
 qed simp
 
-subsection%unimportant\<open>Explicit formulas for interior and relative interior of convex hull\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Explicit formulas for interior and relative interior of convex hull\<close>
 
 lemma at_within_cbox_finite:
   assumes "x \<in> box a b" "x \<notin> S" "finite S"
   shows "(at x within cbox a b - S) = at x"
 proof -

   assume ?rhs
   then show ?lhs
     by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
 qed
 
-subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Similar results for closure and (relative or absolute) frontier\<close>
 
 lemma closure_convex_hull [simp]:
   fixes s :: "'a::euclidean_space set"
   shows "compact s ==> closure(convex hull s) = convex hull s"
   by (simp add: compact_imp_closed compact_convex_hull)

 qed
 
 
 subsection \<open>Coplanarity, and collinearity in terms of affine hull\<close>
 
-definition%important coplanar  where
+definition\<^marker>\<open>tag important\<close> coplanar  where
    "coplanar s \<equiv> \<exists>u v w. s \<subseteq> affine hull {u,v,w}"
 
 lemma collinear_affine_hull:
   "collinear s \<longleftrightarrow> (\<exists>u v. s \<subseteq> affine hull {u,v})"
 proof (cases "s={}")

 apply (rule_tac x="\<lambda>r. (if r=a then x else if r=b then y else if r=c then z else 0)" in exI)
 apply simp
 done
 
 
-subsection%unimportant\<open>Basic lemmas about hyperplanes and halfspaces\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic lemmas about hyperplanes and halfspaces\<close>
 
 lemma halfspace_Int_eq:
      "{x. a \<bullet> x \<le> b} \<inter> {x. b \<le> a \<bullet> x} = {x. a \<bullet> x = b}"
      "{x. b \<le> a \<bullet> x} \<inter> {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
   by auto

 lemma halfspace_eq_empty_ge:
    "{x. a \<bullet> x \<ge> b} = {} \<longleftrightarrow> a = 0 \<and> b > 0"
 using halfspace_eq_empty_le [of "-a" "-b"]
 by simp
 
-subsection%unimportant\<open>Use set distance for an easy proof of separation properties\<close>
-
-proposition%unimportant separation_closures:
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Use set distance for an easy proof of separation properties\<close>
+
+proposition\<^marker>\<open>tag unimportant\<close> separation_closures:
   fixes S :: "'a::euclidean_space set"
   assumes "S \<inter> closure T = {}" "T \<inter> closure S = {}"
   obtains U V where "U \<inter> V = {}" "open U" "open V" "S \<subseteq> U" "T \<subseteq> V"
 proof (cases "S = {} \<or> T = {}")
   case True with that show ?thesis by auto

   show ?lhs
     using proper_map [OF _ _ gfim] **
     by (simp add: continuous_on_closed * closedin_imp_subset)
 qed
 
-subsection%unimportant\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
 
 lemma convex_connected_collinear:
   fixes S :: "'a::euclidean_space set"
   assumes "collinear S"
     shows "convex S \<longleftrightarrow> connected S"

     apply (rule closedin_closed_trans [OF _ closed_UNIV])
     apply (rule closedin_compact_projection [OF \<open>compact S\<close>])
     by (simp add: clo closedin_closed_Int)
 qed
 
-subsubsection%unimportant\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
-
-proposition%unimportant affine_hull_convex_Int_nonempty_interior:
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
+
+proposition\<^marker>\<open>tag unimportant\<close> affine_hull_convex_Int_nonempty_interior:
   fixes S :: "'a::real_normed_vector set"
   assumes "convex S" "S \<inter> interior T \<noteq> {}"
     shows "affine hull (S \<inter> T) = affine hull S"
 proof
   show "affine hull (S \<inter> T) \<subseteq> affine hull S"

 corollary aff_dim_hyperplane [simp]:
   fixes a :: "'a::euclidean_space"
   shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1"
 by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
 
-subsection%unimportant\<open>Some stepping theorems\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Some stepping theorems\<close>
 
 lemma aff_dim_insert:
   fixes a :: "'a::euclidean_space"
   shows "aff_dim (insert a S) = (if a \<in> affine hull S then aff_dim S else aff_dim S + 1)"
 proof (cases "S = {}")

     by (metis that \<open>a \<noteq> 0\<close> aff_dim_hyperplane)
   then show "bounded {x. a \<bullet> x = r} = (DIM('a) = Suc 0)"
     by (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
 qed
 
-subsection%unimportant\<open>General case without assuming closure and getting non-strict separation\<close>
-
-proposition%unimportant separating_hyperplane_closed_point_inset:
+subsection\<^marker>\<open>tag unimportant\<close>\<open>General case without assuming closure and getting non-strict separation\<close>
+
+proposition\<^marker>\<open>tag unimportant\<close> separating_hyperplane_closed_point_inset:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "closed S" "S \<noteq> {}" "z \<notin> S"
   obtains a b where "a \<in> S" "(a - z) \<bullet> z < b" "\<And>x. x \<in> S \<Longrightarrow> b < (a - z) \<bullet> x"
 proof -
   obtain y where "y \<in> S" and y: "\<And>u. u \<in> S \<Longrightarrow> dist z y \<le> dist z u"

   obtains a b where "a \<in> S" "a \<noteq> 0" "0 < b" "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x > b"
 using separating_hyperplane_closed_point_inset [OF assms]
 by simp (metis \<open>0 \<notin> S\<close>)
 
 
-proposition%unimportant separating_hyperplane_set_0_inspan:
+proposition\<^marker>\<open>tag unimportant\<close> separating_hyperplane_set_0_inspan:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "S \<noteq> {}" "0 \<notin> S"
   obtains a where "a \<in> span S" "a \<noteq> 0" "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> a \<bullet> x"
 proof -
   define k where [abs_def]: "k c = {x. 0 \<le> c \<bullet> x}" for c :: 'a

     using \<open>a \<in> span ((+) (- z) ` S)\<close> affine_hull_insert_span_gen apply blast
     apply (simp_all add: \<open>a \<noteq> 0\<close> szx)
     done
 qed
 
-proposition%unimportant supporting_hyperplane_rel_boundary:
+proposition\<^marker>\<open>tag unimportant\<close> supporting_hyperplane_rel_boundary:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "x \<in> S" and xno: "x \<notin> rel_interior S"
   obtains a where "a \<noteq> 0"
               and "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y"
               and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y"

               and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y"
 using supporting_hyperplane_rel_boundary [of "closure S" x]
 by (metis assms convex_closure convex_rel_interior_closure)
 
 
-subsection%unimportant\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
 
 lemma
   fixes s :: "'a::euclidean_space set"
   assumes "\<not> affine_dependent(s \<union> t)"
     shows convex_hull_Int_subset: "convex hull s \<inter> convex hull t \<subseteq> convex hull (s \<inter> t)" (is ?C)

     then show ?A ?C
       by (auto simp: convex_hull_finite affine_hull_finite)
 qed
 
 
-proposition%unimportant affine_hull_Int:
+proposition\<^marker>\<open>tag unimportant\<close> affine_hull_Int:
   fixes s :: "'a::euclidean_space set"
   assumes "\<not> affine_dependent(s \<union> t)"
     shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t"
 apply (rule subset_antisym)
 apply (simp add: hull_mono)
 by (simp add: affine_hull_Int_subset assms)
 
-proposition%unimportant convex_hull_Int:
+proposition\<^marker>\<open>tag unimportant\<close> convex_hull_Int:
   fixes s :: "'a::euclidean_space set"
   assumes "\<not> affine_dependent(s \<union> t)"
     shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t"
 apply (rule subset_antisym)
 apply (simp add: hull_mono)
 by (simp add: convex_hull_Int_subset assms)
 
-proposition%unimportant
+proposition\<^marker>\<open>tag unimportant\<close>
   fixes s :: "'a::euclidean_space set set"
   assumes "\<not> affine_dependent (\<Union>s)"
     shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A")
       and convex_hull_Inter: "convex hull (\<Inter>s) = (\<Inter>t\<in>s. convex hull t)" (is "?C")
 proof -

   qed
   then show "?A" "?C"
     by auto
 qed
 
-proposition%unimportant in_convex_hull_exchange_unique:
+proposition\<^marker>\<open>tag unimportant\<close> in_convex_hull_exchange_unique:
   fixes S :: "'a::euclidean_space set"
   assumes naff: "\<not> affine_dependent S" and a: "a \<in> convex hull S"
       and S: "T \<subseteq> S" "T' \<subseteq> S"
       and x:  "x \<in> convex hull (insert a T)"
       and x': "x \<in> convex hull (insert a T')"

         by simp
     qed
   qed
 qed
 
-corollary%unimportant convex_hull_exchange_Int:
+corollary\<^marker>\<open>tag unimportant\<close> convex_hull_exchange_Int:
   fixes a  :: "'a::euclidean_space"
   assumes "\<not> affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
   shows "(convex hull (insert a T)) \<inter> (convex hull (insert a T')) =
          convex hull (insert a (T \<inter> T'))"
 apply (rule subset_antisym)

     done
   ultimately show ?thesis
     by (simp add: subs) (metis (lifting) span_eq_iff subs)
 qed
 
-proposition%unimportant affine_hyperplane_sums_eq_UNIV:
+proposition\<^marker>\<open>tag unimportant\<close> affine_hyperplane_sums_eq_UNIV:
   fixes S :: "'a :: euclidean_space set"
   assumes "affine S"
       and "S \<inter> {v. a \<bullet> v = b} \<noteq> {}"
       and "S - {v. a \<bullet> v = b} \<noteq> {}"
     shows "{x + y| x y. x \<in> S \<and> a \<bullet> y = b} = UNIV"

     by (metis dim_less dim_subset inf.cobounded2 inf.orderE inf.strict_boundedE not_le)
   ultimately show ?thesis
     by force
 qed
 
-corollary%unimportant dense_complement_affine:
+corollary\<^marker>\<open>tag unimportant\<close> dense_complement_affine:
   fixes S :: "'a :: euclidean_space set"
   assumes less: "aff_dim T < aff_dim S" and "affine S" shows "closure(S - T) = S"
 proof (cases "S \<inter> T = {}")
   case True
   then show ?thesis

     by (simp add: dense_complement_subspace)
   then show ?thesis
     by (metis closure_translation translation_diff translation_invert)
 qed
 
-corollary%unimportant dense_complement_openin_affine_hull:
+corollary\<^marker>\<open>tag unimportant\<close> dense_complement_openin_affine_hull:
   fixes S :: "'a :: euclidean_space set"
   assumes less: "aff_dim T < aff_dim S"
       and ope: "openin (top_of_set (affine hull S)) S"
     shows "closure(S - T) = closure S"
 proof -

     by (rule closure_openin_Int_closure [OF ope])
   then show ?thesis
     by (metis Int_Diff aff_dim_affine_hull affine_affine_hull dense_complement_affine hull_subset inf.orderE less)
 qed
 
-corollary%unimportant dense_complement_convex:
+corollary\<^marker>\<open>tag unimportant\<close> dense_complement_convex:
   fixes S :: "'a :: euclidean_space set"
   assumes "aff_dim T < aff_dim S" "convex S"
     shows "closure(S - T) = closure S"
 proof
   show "closure (S - T) \<subseteq> closure S"

     using \<open>convex S\<close> rel_interior_rel_open rel_open by blast
   then show "closure S \<subseteq> closure (S - T)"
     by (metis Diff_mono \<open>convex S\<close> closure_mono convex_closure_rel_interior order_refl rel_interior_subset)
 qed
 
-corollary%unimportant dense_complement_convex_closed:
+corollary\<^marker>\<open>tag unimportant\<close> dense_complement_convex_closed:
   fixes S :: "'a :: euclidean_space set"
   assumes "aff_dim T < aff_dim S" "convex S" "closed S"
     shows "closure(S - T) = S"
   by (simp add: assms dense_complement_convex)
 
 
-subsection%unimportant\<open>Parallel slices, etc\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Parallel slices, etc\<close>
 
 text\<open> If we take a slice out of a set, we can do it perpendicularly,
   with the normal vector to the slice parallel to the affine hull.\<close>
 
-proposition%unimportant affine_parallel_slice:
+proposition\<^marker>\<open>tag unimportant\<close> affine_parallel_slice:
   fixes S :: "'a :: euclidean_space set"
   assumes "affine S"
       and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
       and "\<not> (S \<subseteq> {x. a \<bullet> x \<le> b})"
   obtains a' b' where "a' \<noteq> 0"

       apply (auto intro: that finite_subset [OF *])
       done
     qed
 qed
 
-corollary%unimportant paracompact_closed:
+corollary\<^marker>\<open>tag unimportant\<close> paracompact_closed:
   fixes S :: "'a :: {metric_space,second_countable_topology} set"
   assumes "closed S"
       and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
       and "S \<subseteq> \<Union>\<C>"
   obtains \<C>' where "S \<subseteq> \<Union>\<C>'"

                and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
                                finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
   by (rule paracompact_closedin [of UNIV S \<C>]) (auto simp: assms)
 
   
-subsection%unimportant\<open>Closed-graph characterization of continuity\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Closed-graph characterization of continuity\<close>
 
 lemma continuous_closed_graph_gen:
   fixes T :: "'b::real_normed_vector set"
   assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
     shows "closedin (top_of_set (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"

   qed (auto simp: fg)
   then show ?thesis
     by simp
 qed
 
-subsection%unimportant\<open>The union of two collinear segments is another segment\<close>
-
-proposition%unimportant in_convex_hull_exchange:
+subsection\<^marker>\<open>tag unimportant\<close>\<open>The union of two collinear segments is another segment\<close>
+
+proposition\<^marker>\<open>tag unimportant\<close> in_convex_hull_exchange:
   fixes a :: "'a::euclidean_space"
   assumes a: "a \<in> convex hull S" and xS: "x \<in> convex hull S"
   obtains b where "b \<in> S" "x \<in> convex hull (insert a (S - {b}))"
 proof (cases "a \<in> S")
   case True

 qed
 
 
 subsection\<open>Orthogonal complement\<close>
 
-definition%important orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
+definition\<^marker>\<open>tag important\<close> orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
   where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
 
 proposition subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
   unfolding subspace_def orthogonal_comp_def orthogonal_def
   by (auto simp: inner_right_distrib)

   shows "f -` {0} =  (range (adjoint f))\<^sup>\<bottom>"
   apply (auto simp: orthogonal_comp_def orthogonal_def)
   apply (simp add: adjoint_works assms(1) inner_commute)
   by (metis adjoint_works all_zero_iff assms(1) inner_commute)
 
-subsection%unimportant \<open>A non-injective linear function maps into a hyperplane.\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>A non-injective linear function maps into a hyperplane.\<close>
 
 lemma linear_surj_adj_imp_inj:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   assumes "linear f" "surj (adjoint f)"
   shows "inj f"