equal
deleted
inserted
replaced
114 |
114 |
115 end |
115 end |
116 |
116 |
117 subsection {* Pair operations are linear and continuous *} |
117 subsection {* Pair operations are linear and continuous *} |
118 |
118 |
119 interpretation fst!: bounded_linear fst |
119 interpretation fst: bounded_linear fst |
120 apply (unfold_locales) |
120 apply (unfold_locales) |
121 apply (rule fst_add) |
121 apply (rule fst_add) |
122 apply (rule fst_scaleR) |
122 apply (rule fst_scaleR) |
123 apply (rule_tac x="1" in exI, simp add: norm_Pair) |
123 apply (rule_tac x="1" in exI, simp add: norm_Pair) |
124 done |
124 done |
125 |
125 |
126 interpretation snd!: bounded_linear snd |
126 interpretation snd: bounded_linear snd |
127 apply (unfold_locales) |
127 apply (unfold_locales) |
128 apply (rule snd_add) |
128 apply (rule snd_add) |
129 apply (rule snd_scaleR) |
129 apply (rule snd_scaleR) |
130 apply (rule_tac x="1" in exI, simp add: norm_Pair) |
130 apply (rule_tac x="1" in exI, simp add: norm_Pair) |
131 done |
131 done |