more accurate declarations;
authorwenzelm
Mon, 14 Jul 2025 22:58:27 +0200
changeset 82867 75064081894e
parent 82866 bfd8258133a1
child 82868 c2a88a1cd07d
more accurate declarations;
src/HOL/Hahn_Banach/Function_Norm.thy
src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Jul 14 12:23:32 2025 +0200
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Jul 14 22:58:27 2025 +0200
@@ -151,7 +151,7 @@
   then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
 qed
 
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [intro?]:
   assumes "continuous V f norm"
   assumes b: "b \<in> B V f"
   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Jul 14 12:23:32 2025 +0200
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Jul 14 22:58:27 2025 +0200
@@ -19,9 +19,9 @@
 locale seminorm =
   fixes V :: "'a::{minus, plus, zero, uminus} set"
   fixes norm :: "'a \<Rightarrow> real"    (\<open>\<parallel>_\<parallel>\<close>)
-  assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
-    and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
-    and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
+  assumes ge_zero [intro?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
+    and abs_homogenous [intro?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
+    and subadditive [intro?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
 
 declare seminorm.intro [intro?]