# HG changeset patch
# User wenzelm
# Date 1752526707 -7200
# Node ID 75064081894e61b8dbba3fdd4916424e7b10be50
# Parent  bfd8258133a1435c7dde6ab554bf5f567bdb4069
more accurate declarations;

diff -r bfd8258133a1 -r 75064081894e src/HOL/Hahn_Banach/Function_Norm.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"
diff -r bfd8258133a1 -r 75064081894e src/HOL/Hahn_Banach/Normed_Space.thy
--- 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?]