src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 66793 deabce3ccf1f
parent 66641 ff2e0115fea4
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -4696,6 +4696,15 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma interior_atLeastLessThan [simp]:
     1.8 +  fixes a::real shows "interior {a..<b} = {a<..<b}"
     1.9 +  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_semiline)
    1.10 +
    1.11 +lemma interior_lessThanAtMost [simp]:
    1.12 +  fixes a::real shows "interior {a<..b} = {a<..<b}"
    1.13 +  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost_real interior_Int
    1.14 +            interior_interior interior_real_semiline)
    1.15 +
    1.16  lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
    1.17    by (metis interior_atLeastAtMost_real interior_interior)
    1.18