equal
deleted
inserted
replaced
478 |
478 |
479 lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow> |
479 lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow> |
480 ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and> |
480 ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and> |
481 ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F" |
481 ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F" |
482 by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def |
482 by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def |
483 tendsto_complex_iff field_simps bounded_linear_scaleR_left bounded_linear_mult_right) |
483 tendsto_complex_iff algebra_simps bounded_linear_scaleR_left bounded_linear_mult_right) |
484 |
484 |
485 lemma has_field_derivative_Re[derivative_intros]: |
485 lemma has_field_derivative_Re[derivative_intros]: |
486 "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F" |
486 "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F" |
487 unfolding has_vector_derivative_complex_iff by safe |
487 unfolding has_vector_derivative_complex_iff by safe |
488 |
488 |