src/HOL/Analysis/Ordered_Euclidean_Space.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69939 812ce526da33
child 70097 4005298550a6
permissions -rw-r--r--
more strict AFP properties;
lp15@69939
     1
section \<open>Ordered Euclidean Space\<close>
nipkow@69631
     2
immler@54780
     3
theory Ordered_Euclidean_Space
immler@54780
     4
imports
immler@56189
     5
  Cartesian_Euclidean_Space
wenzelm@66453
     6
  "HOL-Library.Product_Order"
immler@54780
     7
begin
immler@54780
     8
ak2110@69730
     9
text \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
immler@54780
    10
immler@54780
    11
class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
immler@54780
    12
  assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
immler@54780
    13
  assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
immler@54780
    14
  assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
immler@54780
    15
  assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
haftmann@69260
    16
  assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x\<in>X. x \<bullet> i) *\<^sub>R i)"
haftmann@69260
    17
  assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x\<in>X. x \<bullet> i) *\<^sub>R i)"
wenzelm@61945
    18
  assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
immler@54780
    19
begin
immler@54780
    20
immler@54780
    21
subclass order
wenzelm@61169
    22
  by standard
immler@54780
    23
    (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
immler@54780
    24
immler@54780
    25
subclass ordered_ab_group_add_abs
wenzelm@61169
    26
  by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
immler@54780
    27
immler@54780
    28
subclass ordered_real_vector
wenzelm@61169
    29
  by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
immler@54780
    30
immler@54780
    31
subclass lattice
wenzelm@61169
    32
  by standard (auto simp: eucl_inf eucl_sup eucl_le)
immler@54780
    33
immler@54780
    34
subclass distrib_lattice
wenzelm@61169
    35
  by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
immler@54780
    36
immler@54780
    37
subclass conditionally_complete_lattice
ak2110@69730
    38
proof
immler@54780
    39
  fix z::'a and X::"'a set"
immler@54780
    40
  assume "X \<noteq> {}"
immler@54780
    41
  hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
immler@54780
    42
  thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
haftmann@62343
    43
    by (auto simp: eucl_Inf eucl_Sup eucl_le
immler@54780
    44
      intro!: cInf_greatest cSup_least)
immler@54780
    45
qed (force intro!: cInf_lower cSup_upper
immler@54780
    46
      simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
haftmann@62343
    47
        eucl_Inf eucl_Sup eucl_le)+
immler@54780
    48
ak2110@69730
    49
lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
immler@54780
    50
  and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
nipkow@64267
    51
  by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta
immler@54780
    52
      cong: if_cong)
immler@54780
    53
ak2110@69730
    54
lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
haftmann@69260
    55
  and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x\<in>X. f x) \<bullet> i = (SUP x\<in>X. f x \<bullet> i)"
haftmann@69861
    56
  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: image_comp)
immler@54780
    57
ak2110@69730
    58
lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
immler@54780
    59
  by (auto simp: eucl_abs)
immler@54780
    60
ak2110@69730
    61
lemma
immler@54780
    62
  abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
immler@54780
    63
  by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
immler@54780
    64
ak2110@69730
    65
lemma interval_inner_leI:
immler@54780
    66
  assumes "x \<in> {a .. b}" "0 \<le> i"
immler@54780
    67
  shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
immler@54780
    68
  using assms
immler@54780
    69
  unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
nipkow@64267
    70
  by (auto intro!: ordered_comm_monoid_add_class.sum_mono mult_right_mono simp: eucl_le)
immler@54780
    71
ak2110@69730
    72
lemma inner_nonneg_nonneg:
immler@54780
    73
  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
immler@54780
    74
  using interval_inner_leI[of a 0 a b]
immler@54780
    75
  by auto
immler@54780
    76
ak2110@69730
    77
lemma inner_Basis_mono:
immler@54780
    78
  shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
immler@54780
    79
  by (simp add: eucl_le)
immler@54780
    80
ak2110@69730
    81
lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
immler@54780
    82
  by (auto simp: eucl_le inner_Basis)
immler@54780
    83
ak2110@69730
    84
lemma Sup_eq_maximum_componentwise:
immler@54781
    85
  fixes s::"'a set"
immler@54781
    86
  assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
immler@54781
    87
  assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b"
immler@54781
    88
  assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
immler@54781
    89
  shows "Sup s = X"
immler@54781
    90
  using assms
nipkow@64267
    91
  unfolding eucl_Sup euclidean_representation_sum
haftmann@62343
    92
  by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
immler@54781
    93
ak2110@69730
    94
lemma Inf_eq_minimum_componentwise:
immler@54781
    95
  assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
immler@54781
    96
  assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b"
immler@54781
    97
  assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
immler@54781
    98
  shows "Inf s = X"
immler@54781
    99
  using assms
nipkow@64267
   100
  unfolding eucl_Inf euclidean_representation_sum
haftmann@62343
   101
  by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
immler@54781
   102
immler@54780
   103
end
immler@54780
   104
ak2110@69730
   105
proposition  compact_attains_Inf_componentwise:
immler@54781
   106
  fixes b::"'a::ordered_euclidean_space"
immler@54781
   107
  assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
immler@54781
   108
  obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
ak2110@69730
   109
proof atomize_elim
immler@54781
   110
  let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
immler@54781
   111
  from assms have "compact ?proj" "?proj \<noteq> {}"
hoelzl@56371
   112
    by (auto intro!: compact_continuous_image continuous_intros)
immler@54781
   113
  from compact_attains_inf[OF this]
immler@54781
   114
  obtain s x
immler@54781
   115
    where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t"
immler@54781
   116
      and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
immler@54781
   117
    by auto
immler@54781
   118
  hence "Inf ?proj = x \<bullet> b"
haftmann@62343
   119
    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
immler@54781
   120
  hence "x \<bullet> b = Inf X \<bullet> b"
nipkow@64267
   121
    by (auto simp: eucl_Inf inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta
haftmann@56166
   122
      cong: if_cong)
immler@54781
   123
  with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
immler@54781
   124
qed
immler@54781
   125
ak2110@69730
   126
proposition
immler@54781
   127
  compact_attains_Sup_componentwise:
immler@54781
   128
  fixes b::"'a::ordered_euclidean_space"
immler@54781
   129
  assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
immler@54781
   130
  obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
ak2110@69730
   131
proof atomize_elim
immler@54781
   132
  let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
immler@54781
   133
  from assms have "compact ?proj" "?proj \<noteq> {}"
hoelzl@56371
   134
    by (auto intro!: compact_continuous_image continuous_intros)
immler@54781
   135
  from compact_attains_sup[OF this]
immler@54781
   136
  obtain s x
immler@54781
   137
    where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s"
immler@54781
   138
      and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
immler@54781
   139
    by auto
immler@54781
   140
  hence "Sup ?proj = x \<bullet> b"
haftmann@62343
   141
    by (auto intro!: cSup_eq_maximum)
immler@54781
   142
  hence "x \<bullet> b = Sup X \<bullet> b"
nipkow@64267
   143
    by (auto simp: eucl_Sup[where 'a='a] inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta
haftmann@62343
   144
      cong: if_cong)
immler@54781
   145
  with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
immler@54781
   146
qed
immler@54781
   147
ak2110@69730
   148
lemma (in order) atLeastatMost_empty'[simp]:
nipkow@69508
   149
  "(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
immler@54780
   150
  by (auto)
immler@54780
   151
immler@54780
   152
instance real :: ordered_euclidean_space
haftmann@62343
   153
  by standard auto
immler@54780
   154
ak2110@69730
   155
lemma in_Basis_prod_iff:
immler@54780
   156
  fixes i::"'a::euclidean_space*'b::euclidean_space"
immler@54780
   157
  shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
immler@54780
   158
  by (cases i) (auto simp: Basis_prod_def)
immler@54780
   159
ak2110@69730
   160
instantiation%unimportant prod :: (abs, abs) abs
immler@54780
   161
begin
immler@54780
   162
wenzelm@61945
   163
definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)"
immler@54780
   164
wenzelm@61945
   165
instance ..
wenzelm@61945
   166
immler@54780
   167
end
immler@54780
   168
immler@54780
   169
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
wenzelm@61169
   170
  by standard
nipkow@64267
   171
    (auto intro!: add_mono simp add: euclidean_representation_sum'  Ball_def inner_prod_def
immler@54780
   172
      in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
immler@54780
   173
      inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
immler@54780
   174
      eucl_le[where 'a='b] abs_prod_def abs_inner)
immler@54780
   175
wenzelm@61808
   176
text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
immler@56188
   177
ak2110@69730
   178
proposition
wenzelm@61076
   179
  fixes a :: "'a::ordered_euclidean_space"
immler@56188
   180
  shows cbox_interval: "cbox a b = {a..b}"
immler@56188
   181
    and interval_cbox: "{a..b} = cbox a b"
immler@56188
   182
    and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}"
immler@56188
   183
    and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
ak2110@69730
   184
  by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
immler@56188
   185
ak2110@69730
   186
lemma vec_nth_real_1_iff_cbox [simp]:
lp15@67981
   187
  fixes a b :: real
lp15@67981
   188
  shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
lp15@67981
   189
  by (metis interval_cbox vec_nth_1_iff_cbox)
lp15@67981
   190
ak2110@69730
   191
lemma closed_eucl_atLeastAtMost[simp, intro]:
wenzelm@61076
   192
  fixes a :: "'a::ordered_euclidean_space"
immler@56188
   193
  shows "closed {a..b}"
immler@56188
   194
  by (simp add: cbox_interval[symmetric] closed_cbox)
immler@56188
   195
ak2110@69730
   196
lemma closed_eucl_atMost[simp, intro]:
wenzelm@61076
   197
  fixes a :: "'a::ordered_euclidean_space"
immler@56188
   198
  shows "closed {..a}"
lp15@66827
   199
  by (simp add: closed_interval_left eucl_le_atMost[symmetric])
immler@56188
   200
ak2110@69730
   201
lemma closed_eucl_atLeast[simp, intro]:
wenzelm@61076
   202
  fixes a :: "'a::ordered_euclidean_space"
immler@56188
   203
  shows "closed {a..}"
lp15@66827
   204
  by (simp add: closed_interval_right eucl_le_atLeast[symmetric])
immler@56188
   205
ak2110@69730
   206
lemma bounded_closed_interval [simp]:
immler@56189
   207
  fixes a :: "'a::ordered_euclidean_space"
immler@56189
   208
  shows "bounded {a .. b}"
immler@56189
   209
  using bounded_cbox[of a b]
immler@56189
   210
  by (metis interval_cbox)
immler@56189
   211
ak2110@69730
   212
lemma convex_closed_interval [simp]:
immler@56190
   213
  fixes a :: "'a::ordered_euclidean_space"
immler@56190
   214
  shows "convex {a .. b}"
immler@56190
   215
  using convex_box[of a b]
immler@56190
   216
  by (metis interval_cbox)
immler@56190
   217
ak2110@69730
   218
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
immler@56188
   219
  (if {a .. b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a .. m *\<^sub>R b} else {m *\<^sub>R b .. m *\<^sub>R a})"
immler@56188
   220
  using image_smult_cbox[of m a b]
immler@56188
   221
  by (simp add: cbox_interval)
immler@54780
   222
ak2110@69730
   223
lemma [simp]:
immler@67685
   224
  fixes a b::"'a::ordered_euclidean_space" and r s::real
immler@67685
   225
  shows is_interval_io: "is_interval {..<r}"
immler@67685
   226
    and is_interval_ic: "is_interval {..a}"
immler@67685
   227
    and is_interval_oi: "is_interval {r<..}"
immler@67685
   228
    and is_interval_ci: "is_interval {a..}"
immler@67685
   229
    and is_interval_oo: "is_interval {r<..<s}"
immler@67685
   230
    and is_interval_oc: "is_interval {r<..s}"
immler@67685
   231
    and is_interval_co: "is_interval {r..<s}"
immler@67685
   232
    and is_interval_cc: "is_interval {b..a}"
immler@67685
   233
  by (force simp: is_interval_def eucl_le[where 'a='a])+
immler@67685
   234
lp15@69000
   235
lemma connected_interval [simp]:
lp15@69000
   236
  fixes a b::"'a::ordered_euclidean_space"
lp15@69000
   237
  shows "connected {a..b}"
lp15@69000
   238
  using is_interval_cc is_interval_connected by blast
lp15@69000
   239
lp15@69000
   240
lemma path_connected_interval [simp]:
lp15@69000
   241
  fixes a b::"'a::ordered_euclidean_space"
lp15@69000
   242
  shows "path_connected {a..b}"
lp15@69000
   243
  using is_interval_cc is_interval_path_connected by blast
lp15@69000
   244
lp15@69874
   245
lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
lp15@69874
   246
  by (simp add: convex_imp_path_connected)
lp15@69874
   247
lp15@69874
   248
lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
lp15@69874
   249
  by (simp add: convex_imp_path_connected)
lp15@69874
   250
lp15@69874
   251
lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
lp15@69874
   252
  by (simp add: convex_imp_path_connected)
lp15@69874
   253
lp15@69874
   254
lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
lp15@69874
   255
  by (simp add: convex_imp_path_connected)
lp15@69874
   256
lp15@69874
   257
lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
lp15@69874
   258
  by (simp add: convex_imp_path_connected)
lp15@69874
   259
lp15@69874
   260
lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
lp15@69874
   261
  by (simp add: convex_imp_path_connected)
lp15@69874
   262
lp15@69874
   263
lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
lp15@69874
   264
  by (simp add: convex_imp_path_connected)
lp15@69874
   265
ak2110@69730
   266
lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
immler@67685
   267
  by (auto simp: real_atLeastGreaterThan_eq)
immler@56189
   268
ak2110@69730
   269
lemma compact_interval [simp]:
immler@56190
   270
  fixes a b::"'a::ordered_euclidean_space"
immler@56190
   271
  shows "compact {a .. b}"
immler@56190
   272
  by (metis compact_cbox interval_cbox)
immler@56190
   273
ak2110@69730
   274
lemma homeomorphic_closed_intervals:
lp15@62620
   275
  fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
lp15@62620
   276
  assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
lp15@62620
   277
    shows "(cbox a b) homeomorphic (cbox c d)"
lp15@62620
   278
apply (rule homeomorphic_convex_compact)
lp15@62620
   279
using assms apply auto
lp15@62620
   280
done
lp15@62620
   281
ak2110@69730
   282
lemma homeomorphic_closed_intervals_real:
lp15@62620
   283
  fixes a::real and b and c::real and d
lp15@62620
   284
  assumes "a<b" and "c<d"
lp15@68239
   285
  shows "{a..b} homeomorphic {c..d}"
lp15@68239
   286
  using assms by (auto intro: homeomorphic_convex_compact)
lp15@62620
   287
immler@54780
   288
no_notation
immler@54780
   289
  eucl_less (infix "<e" 50)
immler@54780
   290
ak2110@69730
   291
lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
nipkow@64267
   292
  by (auto intro: sum_nonneg)
immler@56189
   293
ak2110@69730
   294
lemma
immler@56190
   295
  fixes a b::"'a::ordered_euclidean_space"
immler@56190
   296
  shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
immler@56190
   297
    and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
immler@56190
   298
    and bdd_above_box[intro, simp]: "bdd_above (box a b)"
immler@56190
   299
    and bdd_below_box[intro, simp]: "bdd_below (box a b)"
immler@56190
   300
  unfolding atomize_conj
immler@56190
   301
  by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
lp15@68120
   302
            bounded_subset_cbox_symmetric interval_cbox)
immler@56190
   303
immler@56189
   304
instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
immler@56189
   305
begin
immler@56189
   306
ak2110@68833
   307
definition%important "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
ak2110@68833
   308
definition%important "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
haftmann@69260
   309
definition%important "Inf X = (\<chi> i. (INF x\<in>X. x $ i))"
haftmann@69260
   310
definition%important "Sup X = (\<chi> i. (SUP x\<in>X. x $ i))"
ak2110@68833
   311
definition%important "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
immler@56189
   312
immler@56189
   313
instance
wenzelm@61169
   314
  apply standard
nipkow@64267
   315
  unfolding euclidean_representation_sum'
immler@56189
   316
  apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
immler@56189
   317
    Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
immler@56189
   318
    inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
immler@56189
   319
  done
immler@56189
   320
immler@54780
   321
end
immler@56189
   322
ak2110@69730
   323
lemma ANR_interval [iff]:
lp15@63469
   324
    fixes a :: "'a::ordered_euclidean_space"
lp15@63469
   325
    shows "ANR{a..b}"
lp15@63469
   326
by (simp add: interval_cbox)
lp15@63469
   327
ak2110@69730
   328
lemma ENR_interval [iff]:
lp15@63469
   329
    fixes a :: "'a::ordered_euclidean_space"
lp15@63469
   330
    shows "ENR{a..b}"
lp15@63469
   331
  by (auto simp: interval_cbox)
lp15@63469
   332
immler@56189
   333
end
immler@56189
   334