[STATEMENT]
lemma picard_lindeloef_sq_mtx_affine:
  assumes "continuous_on T A" and "continuous_on T B" 
    and "t\<^sub>0 \<in> T" "is_interval T" "open T" and "open S"
  shows "picard_lindeloef (\<lambda>t s. A t *\<^sub>V s + B t) T S t\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. picard_lindeloef (\<lambda>t s. A t *\<^sub>V s + B t) T S t\<^sub>0
[PROOF STEP]
apply(unfold_locales, simp_all add: assms, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> S \<Longrightarrow> continuous_on T (\<lambda>t. A t *\<^sub>V s + B t)
 2. local_lipschitz T S (\<lambda>t s. A t *\<^sub>V s + B t)
[PROOF STEP]
using continuous_on_affine assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on ?s ?A; continuous_on ?s ?g\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. ?A x *\<^sub>V ?sa + ?g x)
continuous_on T A
continuous_on T B
t\<^sub>0 \<in> T
is_interval T
open T
open S

goal (2 subgoals):
 1. \<And>s. s \<in> S \<Longrightarrow> continuous_on T (\<lambda>t. A t *\<^sub>V s + B t)
 2. local_lipschitz T S (\<lambda>t s. A t *\<^sub>V s + B t)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_lipschitz T S (\<lambda>t s. A t *\<^sub>V s + B t)
[PROOF STEP]
by (rule local_lipschitz_sq_mtx_affine, simp_all add: assms)