equal
deleted
inserted
replaced
17 |
17 |
18 locale norm_syntax = |
18 locale norm_syntax = |
19 fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
19 fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
20 |
20 |
21 locale seminorm = var V + norm_syntax + |
21 locale seminorm = var V + norm_syntax + |
|
22 constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set" |
22 assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>" |
23 assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>" |
23 and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" |
24 and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" |
24 and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" |
25 and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" |
25 |
26 |
26 declare seminorm.intro [intro?] |
27 declare seminorm.intro [intro?] |