[STATEMENT]
lemma closedin_standard_simplex:
   "closedin (powertop_real UNIV) (standard_simplex p)"
    (is "closedin ?X ?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
have eq: "standard_simplex p =
              (\<Inter>i. {x. x \<in> topspace ?X \<and> x i \<in> {0..1}}) \<inter>
              (\<Inter>i \<in> {p<..}. {x \<in> topspace ?X. x i \<in> {0}}) \<inter>
              {x \<in> topspace ?X. (\<Sum>i\<le>p. x i) \<in> {1}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. standard_simplex p = (\<Inter>i. {x \<in> topspace (powertop_real UNIV). x i \<in> {0..1}}) \<inter> (\<Inter>i\<in>{p<..}. {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}) \<inter> {x \<in> topspace (powertop_real UNIV). sum x {..p} \<in> {1}}
[PROOF STEP]
by (auto simp: standard_simplex_def topspace_product_topology)
[PROOF STATE]
proof (state)
this:
standard_simplex p = (\<Inter>i. {x \<in> topspace (powertop_real UNIV). x i \<in> {0..1}}) \<inter> (\<Inter>i\<in>{p<..}. {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}) \<inter> {x \<in> topspace (powertop_real UNIV). sum x {..p} \<in> {1}}

goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
unfolding eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) ((\<Inter>i. {x \<in> topspace (powertop_real UNIV). x i \<in> {0..1}}) \<inter> (\<Inter>i\<in>{p<..}. {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}) \<inter> {x \<in> topspace (powertop_real UNIV). sum x {..p} \<in> {1}})
[PROOF STEP]
by (rule closedin_Int closedin_Inter continuous_map_sum
             continuous_map_product_projection closedin_continuous_map_preimage | force | clarify)+
[PROOF STATE]
proof (state)
this:
closedin (powertop_real UNIV) (standard_simplex p)

goal:
No subgoals!
[PROOF STEP]
qed