equal
deleted
inserted
replaced
6047 have fh': "f holomorphic_on cball z ((r + dist w z) / 2)" |
6047 have fh': "f holomorphic_on cball z ((r + dist w z) / 2)" |
6048 apply (rule holomorphic_on_subset [OF holf]) |
6048 apply (rule holomorphic_on_subset [OF holf]) |
6049 apply (clarsimp simp del: divide_const_simps) |
6049 apply (clarsimp simp del: divide_const_simps) |
6050 apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w) |
6050 apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w) |
6051 done |
6051 done |
6052 --\<open>Replacing @{term r} and the original (weak) premises\<close> |
6052 \<comment>\<open>Replacing @{term r} and the original (weak) premises\<close> |
6053 obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r" |
6053 obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r" |
6054 apply (rule that [of "(r + dist w z) / 2"]) |
6054 apply (rule that [of "(r + dist w z) / 2"]) |
6055 apply (simp_all add: fh') |
6055 apply (simp_all add: fh') |
6056 apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w) |
6056 apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w) |
6057 apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w) |
6057 apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w) |