src/HOL/Analysis/Bounded_Continuous_Function.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69861 62e47f06d22c
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
wenzelm@60420
     1
section \<open>Bounded Continuous Functions\<close>
wenzelm@60421
     2
hoelzl@59453
     3
theory Bounded_Continuous_Function
immler@65204
     4
  imports
immler@65204
     5
    Henstock_Kurzweil_Integration
hoelzl@59453
     6
begin
hoelzl@59453
     7
wenzelm@60421
     8
subsection \<open>Definition\<close>
hoelzl@59453
     9
immler@68838
    10
definition%important "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
hoelzl@59453
    11
immler@65204
    12
typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
immler@65205
    13
  "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
immler@65204
    14
  morphisms apply_bcontfun Bcontfun
immler@65205
    15
  by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
immler@65204
    16
immler@65204
    17
declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
immler@65204
    18
immler@65204
    19
setup_lifting type_definition_bcontfun
immler@65204
    20
immler@65204
    21
lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
immler@65204
    22
  and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
immler@65204
    23
  using apply_bcontfun[of x]
immler@65205
    24
  by (auto simp: bcontfun_def intro: continuous_on_subset)
immler@65204
    25
immler@65204
    26
lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
immler@65204
    27
  by transfer auto
hoelzl@59453
    28
hoelzl@59453
    29
lemma bcontfunE:
immler@65205
    30
  assumes "f \<in> bcontfun"
immler@65204
    31
  obtains g where "f = apply_bcontfun g"
immler@65205
    32
  by (blast intro: apply_bcontfun_cases assms )
immler@65205
    33
immler@65205
    34
lemma const_bcontfun: "(\<lambda>x. b) \<in> bcontfun"
immler@65205
    35
  by (auto simp: bcontfun_def continuous_on_const image_def)
hoelzl@59453
    36
immler@65204
    37
lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
immler@65205
    38
  by (rule const_bcontfun)
hoelzl@59453
    39
hoelzl@62101
    40
(* TODO: Generalize to uniform spaces? *)
hoelzl@59453
    41
instantiation bcontfun :: (topological_space, metric_space) metric_space
hoelzl@59453
    42
begin
hoelzl@59453
    43
immler@68838
    44
lift_definition%important dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
immler@65204
    45
  is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
hoelzl@59453
    46
immler@65204
    47
definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
haftmann@69260
    48
  where "uniformity_bcontfun = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
hoelzl@62101
    49
immler@65204
    50
definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
hoelzl@62101
    51
  where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
hoelzl@59453
    52
immler@65204
    53
lemma bounded_dist_le_SUP_dist:
immler@65204
    54
  "bounded (range f) \<Longrightarrow> bounded (range g) \<Longrightarrow> dist (f x) (g x) \<le> (SUP x. dist (f x) (g x))"
immler@65204
    55
  by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp)
immler@65204
    56
hoelzl@59453
    57
lemma dist_bounded:
immler@65204
    58
  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
immler@65204
    59
  shows "dist (f x) (g x) \<le> dist f g"
immler@65205
    60
  by transfer (auto intro!: bounded_dist_le_SUP_dist simp: bcontfun_def)
hoelzl@59453
    61
hoelzl@59453
    62
lemma dist_bound:
immler@65204
    63
  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
immler@65204
    64
  assumes "\<And>x. dist (f x) (g x) \<le> b"
hoelzl@59453
    65
  shows "dist f g \<le> b"
immler@65204
    66
  using assms
immler@65204
    67
  by transfer (auto intro!: cSUP_least)
hoelzl@59453
    68
hoelzl@59453
    69
lemma dist_fun_lt_imp_dist_val_lt:
immler@65204
    70
  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
hoelzl@59453
    71
  assumes "dist f g < e"
immler@65204
    72
  shows "dist (f x) (g x) < e"
hoelzl@59453
    73
  using dist_bounded assms by (rule le_less_trans)
hoelzl@59453
    74
hoelzl@59453
    75
instance
hoelzl@59453
    76
proof
immler@65204
    77
  fix f g h :: "'a \<Rightarrow>\<^sub>C 'b"
hoelzl@59453
    78
  show "dist f g = 0 \<longleftrightarrow> f = g"
hoelzl@59453
    79
  proof
immler@65204
    80
    have "\<And>x. dist (f x) (g x) \<le> dist f g"
wenzelm@60421
    81
      by (rule dist_bounded)
hoelzl@59453
    82
    also assume "dist f g = 0"
wenzelm@60421
    83
    finally show "f = g"
immler@65204
    84
      by (auto simp: apply_bcontfun_inject[symmetric])
haftmann@62343
    85
  qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
hoelzl@59453
    86
  show "dist f g \<le> dist f h + dist g h"
immler@65204
    87
  proof (rule dist_bound)
hoelzl@59453
    88
    fix x
immler@65204
    89
    have "dist (f x) (g x) \<le> dist (f x) (h x) + dist (g x) (h x)"
hoelzl@59453
    90
      by (rule dist_triangle2)
immler@65204
    91
    also have "dist (f x) (h x) \<le> dist f h"
wenzelm@60421
    92
      by (rule dist_bounded)
immler@65204
    93
    also have "dist (g x) (h x) \<le> dist g h"
wenzelm@60421
    94
      by (rule dist_bounded)
immler@65204
    95
    finally show "dist (f x) (g x) \<le> dist f h + dist g h"
wenzelm@60421
    96
      by simp
hoelzl@59453
    97
  qed
hoelzl@62101
    98
qed (rule open_bcontfun_def uniformity_bcontfun_def)+
wenzelm@60421
    99
hoelzl@59453
   100
end
hoelzl@59453
   101
immler@65204
   102
lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set"
immler@65205
   103
  is "\<lambda>I X. Pi I X \<inter> bcontfun"
immler@65204
   104
  by auto
immler@65204
   105
immler@65204
   106
lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X"
immler@65204
   107
  by transfer simp
immler@65204
   108
immler@65204
   109
lemmas mem_PiCD = mem_PiC_iff[THEN iffD1]
immler@65204
   110
  and mem_PiCI = mem_PiC_iff[THEN iffD2]
immler@65204
   111
immler@65204
   112
lemma tendsto_bcontfun_uniform_limit:
immler@65204
   113
  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
immler@65204
   114
  assumes "(f \<longlongrightarrow> l) F"
immler@65204
   115
  shows "uniform_limit UNIV f l F"
immler@65204
   116
proof (rule uniform_limitI)
immler@65204
   117
  fix e::real assume "e > 0"
immler@65204
   118
  from tendstoD[OF assms this] have "\<forall>\<^sub>F x in F. dist (f x) l < e" .
immler@65204
   119
  then show "\<forall>\<^sub>F n in F. \<forall>x\<in>UNIV. dist ((f n) x) (l x) < e"
immler@65204
   120
    by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt)
immler@65204
   121
qed
immler@65204
   122
immler@65204
   123
lemma uniform_limit_tendsto_bcontfun:
immler@65204
   124
  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
immler@65204
   125
    and l::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
immler@65204
   126
  assumes "uniform_limit UNIV f l F"
immler@65204
   127
  shows "(f \<longlongrightarrow> l) F"
immler@65204
   128
proof (rule tendstoI)
immler@65204
   129
  fix e::real assume "e > 0"
immler@65204
   130
  then have "e / 2 > 0" by simp
immler@65204
   131
  from uniform_limitD[OF assms this]
immler@65204
   132
  have "\<forall>\<^sub>F i in F. \<forall>x. dist (f i x) (l x) < e / 2" by simp
immler@65204
   133
  then have "\<forall>\<^sub>F x in F. dist (f x) l \<le> e / 2"
immler@65204
   134
    by eventually_elim (blast intro: dist_bound less_imp_le)
immler@65204
   135
  then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
immler@65204
   136
    by eventually_elim (use \<open>0 < e\<close> in auto)
immler@65204
   137
qed
immler@65204
   138
immler@65204
   139
lemma uniform_limit_bcontfunE:
immler@65204
   140
  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
immler@65204
   141
    and l::"'a::topological_space \<Rightarrow> 'b::metric_space"
immler@65204
   142
  assumes "uniform_limit UNIV f l F" "F \<noteq> bot"
immler@65204
   143
  obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
immler@65204
   144
  where "l = l'" "(f \<longlongrightarrow> l') F"
immler@65204
   145
  by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
immler@65205
   146
      bcontfun_def mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun
immler@65205
   147
      uniform_limit_theorem)
immler@65204
   148
immler@65204
   149
lemma closed_PiC:
wenzelm@60421
   150
  fixes I :: "'a::metric_space set"
wenzelm@60421
   151
    and X :: "'a \<Rightarrow> 'b::complete_space set"
hoelzl@59453
   152
  assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
immler@65204
   153
  shows "closed (PiC I X)"
hoelzl@59453
   154
  unfolding closed_sequential_limits
hoelzl@59453
   155
proof safe
hoelzl@59453
   156
  fix f l
immler@65204
   157
  assume seq: "\<forall>n. f n \<in> PiC I X" and lim: "f \<longlonglongrightarrow> l"
immler@65204
   158
  show "l \<in> PiC I X"
immler@65204
   159
  proof (safe intro!: mem_PiCI)
hoelzl@59453
   160
    fix x assume "x \<in> I"
wenzelm@60421
   161
    then have "closed (X x)"
wenzelm@60421
   162
      using assms by simp
immler@65204
   163
    moreover have "eventually (\<lambda>i. f i x \<in> X x) sequentially"
immler@65204
   164
      using seq \<open>x \<in> I\<close>
immler@65204
   165
      by (auto intro!: eventuallyI dest!: mem_PiCD simp: Pi_iff)
hoelzl@59453
   166
    moreover note sequentially_bot
immler@65204
   167
    moreover have "(\<lambda>n. (f n) x) \<longlonglongrightarrow> l x"
immler@65204
   168
      using tendsto_bcontfun_uniform_limit[OF lim]
immler@65204
   169
      by (rule tendsto_uniform_limitI) simp
immler@65204
   170
    ultimately show "l x \<in> X x"
hoelzl@59453
   171
      by (rule Lim_in_closed_set)
immler@65204
   172
  qed
hoelzl@59453
   173
qed
hoelzl@59453
   174
wenzelm@60421
   175
wenzelm@60420
   176
subsection \<open>Complete Space\<close>
hoelzl@59453
   177
immler@68838
   178
instance%important bcontfun :: (metric_space, complete_space) complete_space
immler@68838
   179
proof%unimportant
wenzelm@60421
   180
  fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
wenzelm@61808
   181
  assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
immler@65204
   182
  then obtain g where "uniform_limit UNIV f g sequentially"
immler@65204
   183
    using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" f]
immler@65204
   184
    unfolding Cauchy_def uniform_limit_sequentially_iff
wenzelm@60421
   185
    by (metis dist_fun_lt_imp_dist_val_lt)
hoelzl@59453
   186
immler@65204
   187
  from uniform_limit_bcontfunE[OF this sequentially_bot]
immler@65204
   188
  obtain l' where "g = apply_bcontfun l'" "(f \<longlonglongrightarrow> l')" by metis
immler@65204
   189
  then show "convergent f"
immler@65204
   190
    by (intro convergentI)
hoelzl@59453
   191
qed
hoelzl@59453
   192
wenzelm@60421
   193
immler@68838
   194
subsection%unimportant \<open>Supremum norm for a normed vector space\<close>
hoelzl@59453
   195
immler@68838
   196
instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_vector
hoelzl@59453
   197
begin
hoelzl@59453
   198
immler@65205
   199
lemma uminus_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. - f x) \<in> bcontfun" for f::"'a \<Rightarrow> 'b"
immler@65205
   200
  by (auto simp: bcontfun_def intro!: continuous_intros)
immler@65205
   201
immler@65205
   202
lemma plus_cont: "f \<in> bcontfun \<Longrightarrow> g \<in> bcontfun \<Longrightarrow> (\<lambda>x. f x + g x) \<in> bcontfun" for f g::"'a \<Rightarrow> 'b"
immler@65205
   203
  by (auto simp: bcontfun_def intro!: continuous_intros bounded_plus_comp)
immler@65205
   204
immler@65205
   205
lemma minus_cont: "f \<in> bcontfun \<Longrightarrow> g \<in> bcontfun \<Longrightarrow> (\<lambda>x. f x - g x) \<in> bcontfun" for f g::"'a \<Rightarrow> 'b"
immler@65205
   206
  by (auto simp: bcontfun_def intro!: continuous_intros bounded_minus_comp)
immler@65205
   207
immler@65205
   208
lemma scaleR_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun" for f :: "'a \<Rightarrow> 'b"
immler@65205
   209
  by (auto simp: bcontfun_def intro!: continuous_intros bounded_scaleR_comp)
immler@65205
   210
immler@65205
   211
lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
immler@65205
   212
  by (auto simp: bcontfun_def intro: boundedI)
immler@65205
   213
immler@65204
   214
lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x"
immler@65205
   215
  by (rule uminus_cont)
hoelzl@59453
   216
immler@65204
   217
lift_definition plus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x + g x"
immler@65205
   218
  by (rule plus_cont)
hoelzl@59453
   219
immler@65204
   220
lift_definition minus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x - g x"
immler@65205
   221
  by (rule minus_cont)
hoelzl@59453
   222
immler@65204
   223
lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0"
immler@65205
   224
  by (rule const_bcontfun)
hoelzl@59453
   225
immler@65204
   226
lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
immler@65204
   227
  by transfer simp
hoelzl@59453
   228
immler@65204
   229
lift_definition scaleR_bcontfun::"real \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>r g x. r *\<^sub>R g x"
immler@65205
   230
  by (rule scaleR_cont)
hoelzl@59453
   231
immler@65204
   232
lemmas [simp] =
immler@65204
   233
  const_bcontfun.rep_eq
immler@65204
   234
  uminus_bcontfun.rep_eq
immler@65204
   235
  plus_bcontfun.rep_eq
immler@65204
   236
  minus_bcontfun.rep_eq
immler@65204
   237
  zero_bcontfun.rep_eq
immler@65204
   238
  scaleR_bcontfun.rep_eq
hoelzl@59453
   239
hoelzl@59453
   240
hoelzl@59453
   241
instance
immler@65204
   242
  by standard (auto intro!: bcontfun_eqI simp: algebra_simps)
wenzelm@60421
   243
hoelzl@59453
   244
end
hoelzl@59453
   245
immler@65204
   246
lemma bounded_norm_le_SUP_norm:
immler@65204
   247
  "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
immler@65204
   248
  by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
immler@65204
   249
immler@68838
   250
instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_normed_vector
hoelzl@59453
   251
begin
hoelzl@59453
   252
wenzelm@60421
   253
definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
wenzelm@60421
   254
  where "norm_bcontfun f = dist f 0"
hoelzl@59453
   255
hoelzl@59453
   256
definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f"
hoelzl@59453
   257
hoelzl@59453
   258
instance
hoelzl@59453
   259
proof
wenzelm@60421
   260
  fix a :: real
wenzelm@60421
   261
  fix f g :: "('a, 'b) bcontfun"
hoelzl@59453
   262
  show "dist f g = norm (f - g)"
immler@65204
   263
    unfolding norm_bcontfun_def
immler@65204
   264
    by transfer (simp add: dist_norm)
hoelzl@59453
   265
  show "norm (f + g) \<le> norm f + norm g"
hoelzl@59453
   266
    unfolding norm_bcontfun_def
immler@65204
   267
    by transfer
immler@65205
   268
      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm
immler@65205
   269
        simp: dist_norm bcontfun_def)
hoelzl@59453
   270
  show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
immler@65204
   271
    unfolding norm_bcontfun_def
immler@65204
   272
    apply transfer
immler@65204
   273
    by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
immler@65204
   274
      (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
haftmann@69861
   275
        simp: bounded_norm_comp bcontfun_def image_comp)
hoelzl@59453
   276
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
hoelzl@59453
   277
hoelzl@59453
   278
end
hoelzl@59453
   279
hoelzl@59453
   280
lemma norm_bounded:
wenzelm@60421
   281
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
immler@65204
   282
  shows "norm (apply_bcontfun f x) \<le> norm f"
hoelzl@59453
   283
  using dist_bounded[of f x 0]
immler@65204
   284
  by (simp add: dist_norm)
hoelzl@59453
   285
hoelzl@59453
   286
lemma norm_bound:
wenzelm@60421
   287
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
immler@65204
   288
  assumes "\<And>x. norm (apply_bcontfun f x) \<le> b"
hoelzl@59453
   289
  shows "norm f \<le> b"
hoelzl@59453
   290
  using dist_bound[of f 0 b] assms
immler@65204
   291
  by (simp add: dist_norm)
hoelzl@59453
   292
immler@68838
   293
subsection%unimportant \<open>(bounded) continuous extenstion\<close>
hoelzl@59453
   294
hoelzl@59453
   295
lemma integral_clamp:
hoelzl@59453
   296
  "integral {t0::real..clamp t0 t1 x} f =
hoelzl@59453
   297
    (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
hoelzl@59453
   298
  by (auto simp: clamp_def)
hoelzl@59453
   299
immler@65204
   300
lemma continuous_on_interval_bcontfunE:
immler@65204
   301
  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::metric_space"
immler@65204
   302
  assumes "continuous_on {a .. b} f"
immler@65204
   303
  obtains g::"'a \<Rightarrow>\<^sub>C 'b" where
immler@65204
   304
    "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> g x = f x"
immler@65204
   305
    "\<And>x. g x = f (clamp a b x)"
immler@65204
   306
proof -
immler@65204
   307
  define g where "g \<equiv> ext_cont f a b"
immler@65205
   308
  have "g \<in> bcontfun"
immler@65204
   309
    using assms
immler@65205
   310
    by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval bcontfun_def)
immler@65205
   311
      (auto simp: g_def ext_cont_def cbox_interval
immler@65204
   312
        intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
immler@65205
   313
  then obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
immler@65204
   314
  then have "h x = f x" if "a \<le> x" "x \<le> b" for x
immler@65204
   315
    by (auto simp: h[symmetric] g_def cbox_interval that)
immler@65204
   316
  moreover
immler@65204
   317
  have "h x = f (clamp a b x)" for x
immler@65204
   318
    by (auto simp: h[symmetric] g_def ext_cont_def)
immler@65204
   319
  ultimately show ?thesis ..
immler@65204
   320
qed
hoelzl@59453
   321
immler@65204
   322
lifting_update bcontfun.lifting
immler@65204
   323
lifting_forget bcontfun.lifting
hoelzl@59453
   324
hoelzl@59453
   325
end