equal
deleted
inserted
replaced
1997 by (simp add: image_subsetI j) |
1997 by (simp add: image_subsetI j) |
1998 have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S" |
1998 have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S" |
1999 using diff_f |
1999 using diff_f |
2000 apply (clarsimp simp add: differentiable_on_def) |
2000 apply (clarsimp simp add: differentiable_on_def) |
2001 apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>] |
2001 apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>] |
2002 linear_imp_differentiable [OF fst_linear]) |
2002 linear_imp_differentiable [OF linear_fst]) |
2003 apply (force simp: image_comp o_def) |
2003 apply (force simp: image_comp o_def) |
2004 done |
2004 done |
2005 have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))" |
2005 have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))" |
2006 by (simp add: o_def) |
2006 by (simp add: o_def) |
2007 then show ?thesis |
2007 then show ?thesis |