equal
deleted
inserted
replaced
210 lemmas bounded_linear_inner_left = |
210 lemmas bounded_linear_inner_left = |
211 bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner] |
211 bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner] |
212 |
212 |
213 lemmas bounded_linear_inner_right = |
213 lemmas bounded_linear_inner_right = |
214 bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner] |
214 bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner] |
|
215 |
|
216 lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose] |
|
217 |
|
218 lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose] |
215 |
219 |
216 lemmas has_derivative_inner_right [derivative_intros] = |
220 lemmas has_derivative_inner_right [derivative_intros] = |
217 bounded_linear.has_derivative [OF bounded_linear_inner_right] |
221 bounded_linear.has_derivative [OF bounded_linear_inner_right] |
218 |
222 |
219 lemmas has_derivative_inner_left [derivative_intros] = |
223 lemmas has_derivative_inner_left [derivative_intros] = |