[STATEMENT]
lemma component_le_infnorm_cart: "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x $ i\<bar> \<le> infnorm x
[PROOF STEP]
using Basis_le_infnorm[of "axis i 1" x]
[PROOF STATE]
proof (prove)
using this:
axis i 1 \<in> Basis \<Longrightarrow> \<bar>x \<bullet> axis i 1\<bar> \<le> infnorm x

goal (1 subgoal):
 1. \<bar>x $ i\<bar> \<le> infnorm x
[PROOF STEP]
by (simp add: Basis_vec_def axis_eq_axis inner_axis)