[STATEMENT]
lemma dim_openin:
  fixes S :: "'a::euclidean_space set"
  assumes ope: "openin (top_of_set T) S" and "subspace T" "S \<noteq> {}"
  shows "dim S = dim T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim S = dim T
[PROOF STEP]
proof (rule order_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dim S \<le> dim T
 2. dim T \<le> dim S
[PROOF STEP]
show "dim S \<le> dim T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim S \<le> dim T
[PROOF STEP]
by (metis ope dim_subset openin_subset topspace_euclidean_subtopology)
[PROOF STATE]
proof (state)
this:
dim S \<le> dim T

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
have "dim T = aff_dim S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (dim T) = aff_dim S
[PROOF STEP]
using aff_dim_openin
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>openin (top_of_set ?T) ?S; affine ?T; ?S \<noteq> {}\<rbrakk> \<Longrightarrow> aff_dim ?S = aff_dim ?T

goal (1 subgoal):
 1. int (dim T) = aff_dim S
[PROOF STEP]
by (metis aff_dim_subspace \<open>subspace T\<close> \<open>S \<noteq> {}\<close> ope subspace_affine)
[PROOF STATE]
proof (state)
this:
int (dim T) = aff_dim S

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (dim T) = aff_dim S

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
have "... \<le> dim S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aff_dim S \<le> int (dim S)
[PROOF STEP]
by (metis aff_dim_subset aff_dim_subspace dim_span span_superset
        subspace_span)
[PROOF STATE]
proof (state)
this:
aff_dim S \<le> int (dim S)

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (dim T) \<le> int (dim S)
[PROOF STEP]
show "dim T \<le> dim S"
[PROOF STATE]
proof (prove)
using this:
int (dim T) \<le> int (dim S)

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim T \<le> dim S

goal:
No subgoals!
[PROOF STEP]
qed