--- 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?]