[STATEMENT]
lemma Fejer_kernel_continuous:
  "continuous_on {-pi..pi} (Fejer_kernel n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {- pi..pi} (Fejer_kernel n)
[PROOF STEP]
apply (rule continuous_on_subset [OF Fejer_kernel_continuous_strong])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {- pi..pi} \<subseteq> {- (2 * pi)<..<2 * pi}
[PROOF STEP]
apply (simp add: subset_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. - pi \<le> t \<and> t \<le> pi \<longrightarrow> - (2 * pi) < t \<and> t < 2 * pi
[PROOF STEP]
using pi_gt_zero
[PROOF STATE]
proof (prove)
using this:
0 < pi

goal (1 subgoal):
 1. \<forall>t. - pi \<le> t \<and> t \<le> pi \<longrightarrow> - (2 * pi) < t \<and> t < 2 * pi
[PROOF STEP]
apply linarith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done