equal
deleted
inserted
replaced
1298 |
1298 |
1299 lemma infnorm_set_lemma_cart: |
1299 lemma infnorm_set_lemma_cart: |
1300 shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}" |
1300 shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}" |
1301 and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}" |
1301 and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}" |
1302 unfolding infnorm_set_image_cart |
1302 unfolding infnorm_set_image_cart |
1303 by (auto intro: finite_imageI) |
1303 by auto |
1304 |
1304 |
1305 lemma component_le_infnorm_cart: |
1305 lemma component_le_infnorm_cart: |
1306 shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)" |
1306 shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)" |
1307 unfolding nth_conv_component |
1307 unfolding nth_conv_component |
1308 using component_le_infnorm[of x] . |
1308 using component_le_infnorm[of x] . |