# 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 \ B V f" shows "b \ \f\\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 \ real" (\\_\\) - assumes ge_zero [iff?]: "x \ V \ 0 \ \x\" - and abs_homogenous [iff?]: "x \ V \ \a \ x\ = \a\ * \x\" - and subadditive [iff?]: "x \ V \ y \ V \ \x + y\ \ \x\ + \y\" + assumes ge_zero [intro?]: "x \ V \ 0 \ \x\" + and abs_homogenous [intro?]: "x \ V \ \a \ x\ = \a\ * \x\" + and subadditive [intro?]: "x \ V \ y \ V \ \x + y\ \ \x\ + \y\" declare seminorm.intro [intro?]