Theory Restriction_Spaces.Restriction_Spaces_Topology

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Benjamin Puyobro, Université Paris-Saclay,
           IRT SystemX, CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section ‹Topological Notions›

(*<*)
theory Restriction_Spaces_Topology
  imports Restriction_Spaces_Prod Restriction_Spaces_Fun
begin
  (*>*)


named_theorems restriction_cont_simpset ― ‹For future automation.›

subsection ‹Continuity›

context restriction begin

definition restriction_cont_at :: ‹['b :: restriction ⇒ 'a, 'b] ⇒ bool›
  (‹cont↓ (_) at (_)› [1000, 1000])
  where ‹cont↓ f at Σ ≡ ∀σ. σ ─↓→ Σ ⟶ (λn. f (σ n)) ─↓→ f Σ›

lemma restriction_cont_atI : ‹(⋀σ. σ ─↓→ Σ ⟹ (λn. f (σ n)) ─↓→ f Σ) ⟹ cont↓ f at Σ›
  by (simp add: restriction_cont_at_def)

lemma restriction_cont_atD : ‹cont↓ f at Σ ⟹ σ ─↓→ Σ ⟹ (λn. f (σ n)) ─↓→ f Σ›
  by (simp add: restriction_cont_at_def)

lemma restriction_cont_at_comp [restriction_cont_simpset] :
  ‹cont↓ f at Σ ⟹ cont↓ g at (f Σ) ⟹ cont↓ (λx. g (f x)) at Σ›
  by (simp add: restriction_cont_at_def restriction_class.restriction_cont_at_def)

lemma restriction_cont_at_if_then_else [restriction_cont_simpset] :
  ‹⟦⋀x. P x ⟹ cont↓ (f x) at Σ; ⋀x. ¬ P x ⟹ cont↓ (g x) at Σ⟧
   ⟹ cont↓ (λy. if P x then f x y else g x y) at Σ›
  by (auto intro!: restriction_cont_atI) (blast dest: restriction_cont_atD)+



definition restriction_open :: ‹'a set ⇒ bool› (‹open↓›)
  where ‹open↓ U ≡ ∀Σ∈U. ∀σ. σ ─↓→ Σ ⟶ (∃n0. ∀k≥n0. σ k ∈ U)›

lemma restriction_openI : ‹(⋀Σ σ. Σ ∈ U ⟹ σ ─↓→ Σ ⟹ ∃n0. ∀k≥n0. σ k ∈ U) ⟹ open↓ U›
  by (simp add: restriction_open_def)

lemma restriction_openD : ‹open↓ U ⟹ Σ ∈ U ⟹ σ ─↓→ Σ ⟹ ∃n0. ∀k≥n0. σ k ∈ U›
  by (simp add: restriction_open_def)

lemma restriction_openE :
  ‹open↓ U ⟹ Σ ∈ U ⟹ σ ─↓→ Σ ⟹ (⋀n0. (⋀n. n0 ≤ k ⟹ σ k ∈ U) ⟹ thesis) ⟹ thesis›
  using restriction_openD by blast

lemma restriction_open_UNIV  [simp] : ‹open↓ UNIV›
  and restriction_open_empty [simp] : ‹open↓ {}›
  by (simp_all add: restriction_open_def)


lemma restriction_open_union :
  ‹open↓ U ⟹ open↓ V ⟹ open↓ (U ∪ V)›
  by (metis Un_iff restriction_open_def)

lemma restriction_open_Union :
  ‹(⋀i. i ∈ I ⟹ open↓ (U i)) ⟹ open↓ (⋃i∈I. U i)›
  by (rule restriction_openI) (metis UN_iff restriction_openD)

lemma restriction_open_inter :
  ‹open↓ (U ∩ V)› if ‹open↓ U› and ‹open↓ V›
proof (rule restriction_openI)
  fix Σ σ assume ‹Σ ∈ U ∩ V› ‹σ ─↓→ Σ›
  from ‹Σ ∈ U ∩ V› have ‹Σ ∈ U› and ‹Σ ∈ V› by simp_all
  from ‹open↓ U› ‹Σ ∈ U› ‹σ ─↓→ Σ› restriction_openD
  obtain n0 where ‹∀k≥n0. σ k ∈ U› by blast
  moreover from ‹open↓ V› ‹Σ ∈ V› ‹σ ─↓→ Σ› restriction_openD
  obtain n1 where ‹∀k≥n1. σ k ∈ V› by blast
  ultimately have ‹∀k≥max n0 n1. σ k ∈ U ∩ V› by simp
  thus ‹∃n0. ∀k≥n0. σ k ∈ U ∩ V› by blast
qed

lemma restriction_open_finite_Inter :
  ‹finite I ⟹ (⋀i. i ∈ I ⟹ open↓ (U i)) ⟹ open↓ (⋂i∈I. U i)›
  by (induct I rule: finite_induct)
    (simp_all add: restriction_open_inter)



definition restriction_closed :: ‹'a set ⇒ bool› (‹closed↓›)
  where ‹closed↓ S ≡ open↓ (- S)›

lemma restriction_closedI : ‹(⋀Σ σ. Σ ∉ S ⟹ σ ─↓→ Σ ⟹ ∃n0. ∀k≥n0. σ k ∉ S) ⟹ closed↓ S›
  by (simp add: restriction_closed_def restriction_open_def)

lemma restriction_closedD : ‹closed↓ S ⟹ Σ ∉ S ⟹ σ ─↓→ Σ ⟹ ∃n0. ∀k≥n0. σ k ∉ S›
  by (simp add: restriction_closed_def restriction_open_def)

lemma restriction_closedE :
  ‹closed↓ S ⟹ Σ ∉ S ⟹ σ ─↓→ Σ ⟹ (⋀n0. (⋀n. n0 ≤ k ⟹ σ k ∉ S) ⟹ thesis) ⟹ thesis›
  using restriction_closedD by blast

lemma restriction_closed_UNIV  [simp] : ‹closed↓ UNIV›
  and restriction_closed_empty [simp] : ‹closed↓ {}›
  by (simp_all add: restriction_closed_def)

end


subsection ‹Balls›

context restriction begin

definition restriction_cball :: ‹'a ⇒ nat ⇒ 'a set› (‹ℬ↓'(_, _')›)
  where ‹ℬ↓(a, n) ≡ {x. x ↓ n = a ↓ n}›

lemma restriction_cball_mem_iff : ‹x ∈ ℬ↓(a, n) ⟷  x ↓ n = a ↓ n›
  and restriction_cball_memI    : ‹x ↓ n = a ↓ n ⟹ x ∈ ℬ↓(a, n)›
  and restriction_cball_memD    : ‹x ∈ ℬ↓(a, n) ⟹ x ↓ n = a ↓ n›
  by (simp_all add: restriction_cball_def)



abbreviation (iff) restriction_ball :: ‹'a ⇒ nat ⇒ 'a set›
  where ‹restriction_ball a n ≡ ℬ↓(a, Suc n)›

lemma ‹x ∈ restriction_ball a n ⟷  x ↓ Suc n = a ↓ Suc n›
  and ‹x ↓ Suc n = a ↓ Suc n ⟹ x ∈ restriction_ball a n›
  and ‹x ∈ restriction_ball a n ⟹ x ↓ Suc n = a ↓ Suc n›
  by (simp_all add: restriction_cball_def)



lemma ‹a ∈ restriction_ball a n›
  and center_mem_restriction_cball [simp] : ‹a ∈ ℬ↓(a, n)›
  by (simp_all add: restriction_cball_memI)

lemma (in restriction_space) restriction_cball_0_is_UNIV [simp] :
  ‹ℬ↓(a, 0) = UNIV› by (simp add: restriction_cball_def)




lemma every_point_of_restriction_cball_is_centre :
  ‹b ∈ ℬ↓(a, n) ⟹ ℬ↓(a, n) = ℬ↓(b, n)›
  by (simp add: restriction_cball_def)


lemma ‹b ∈ restriction_ball a n ⟹ restriction_ball a n = restriction_ball b n›
  by (simp add: every_point_of_restriction_cball_is_centre)


definition restriction_sphere :: ‹'a ⇒ nat ⇒ 'a set› (‹𝒮↓'(_, _')›)
  where ‹𝒮↓(a, n) ≡ {x. x ↓ n = a ↓ n ∧ x ↓ Suc n ≠ a ↓ Suc n}›

lemma restriction_sphere_mem_iff : ‹x ∈ 𝒮↓(a, n) ⟷ x ↓ n = a ↓ n ∧ x ↓ Suc n ≠ a ↓ Suc n›
  and restriction_sphere_memI    : ‹x ↓ n = a ↓ n ⟹ x ↓ Suc n ≠ a ↓ Suc n ⟹ x ∈ 𝒮↓(a, n)›
  and restriction_sphere_memD1   : ‹x ∈ 𝒮↓(a, n) ⟹ x ↓ n = a ↓ n›
  and restriction_sphere_memD2   : ‹x ∈ 𝒮↓(a, n) ⟹ x ↓ Suc n ≠ a ↓ Suc n›
  by (simp_all add: restriction_sphere_def)

lemma restriction_sphere_is_diff : ‹𝒮↓(a, n) = ℬ↓(a, n) - ℬ↓(a, Suc n)›
  by (simp add: set_eq_iff restriction_sphere_mem_iff restriction_cball_mem_iff)




lemma restriction_open_restriction_cball [simp] : ‹open↓ ℬ↓(a, n)›
  by (metis restriction_cball_mem_iff restriction_tendstoE restriction_openI)

lemma restriction_closed_restriction_cball [simp] : ‹closed↓ ℬ↓(a, n)›
  by (metis restriction_cball_mem_iff restriction_closedI restriction_tendstoE)

lemma restriction_open_Compl_iff : ‹open↓ (- S) ⟷ closed↓ S›
  by (simp add: restriction_closed_def)

lemma restriction_open_restriction_sphere [simp] : ‹open↓ 𝒮↓(a, n)›
  by (simp add: restriction_sphere_is_diff Diff_eq
      restriction_open_Compl_iff restriction_open_inter)

lemma restriction_closed_restriction_sphere : ‹closed↓ 𝒮↓(a, n)›
  by (simp add: restriction_closed_def restriction_sphere_is_diff)
    (simp add: restriction_open_union restriction_open_Compl_iff)

end


context restriction_space begin

lemma restriction_cball_anti_mono : ‹n ≤ m ⟹ ℬ↓(a, m) ⊆ ℬ↓(a, n)›
  by (meson restriction_cball_memD restriction_cball_memI restriction_related_le subsetI)

lemma inside_every_cball_iff_eq : ‹(∀n. x ∈ ℬ↓(Σ, n)) ⟷ x = Σ›
  by (simp add: all_restriction_related_iff_related restriction_cball_mem_iff)



lemma Inf_many_inside_cball_iff_eq : ‹(∃∞n. x ∈ ℬ↓(Σ, n)) ⟷ x = Σ›
  by (unfold INFM_nat_le)
    (meson inside_every_cball_iff_eq nle_le restriction_cball_anti_mono subset_eq)

lemma Inf_many_inside_cball_imp_eq : ‹∃∞n. x ∈ ℬ↓(Σ, n) ⟹ x = Σ›
  by (simp add: Inf_many_inside_cball_iff_eq)



lemma restriction_cballs_disjoint_or_subset :
  ‹ℬ↓(a, n) ∩ ℬ↓(b, m) = {} ∨ ℬ↓(a, n) ⊆ ℬ↓(b, m) ∨ ℬ↓(b, m) ⊆ ℬ↓(a, n)›
proof (unfold disj_imp, intro impI)
  assume ‹ℬ↓(a, n) ∩ ℬ↓(b, m) ≠ {}› ‹¬ ℬ↓(a, n) ⊆ ℬ↓(b, m)›
  from ‹ℬ↓(a, n) ∩ ℬ↓(b, m) ≠ {}› obtain x where ‹x ∈ ℬ↓(a, n)› ‹x ∈ ℬ↓(b, m)› by blast
  with every_point_of_restriction_cball_is_centre
  have ‹ℬ↓(a, n) = ℬ↓(x, n)› ‹ℬ↓(b, m) = ℬ↓(x, m)› by auto
  with ‹¬ ℬ↓(a, n) ⊆ ℬ↓(b, m)› show ‹ℬ↓(b, m) ⊆ ℬ↓(a, n)›
    by (metis nle_le restriction_cball_anti_mono)
qed



lemma equal_restriction_to_cball :
  ‹a ∉ ℬ↓(b, n) ⟹ x ∈ ℬ↓(b, n) ⟹ y ∈ ℬ↓(b, n) ⟹ x ↓ k = a ↓ k ⟷ y ↓ k = a ↓ k›
  by (metis nat_le_linear restriction_cball_memD restriction_cball_memI restriction_related_le)

end


context restriction begin

lemma restriction_tendsto_iff_restriction_cball_characterization :
  ‹σ ─↓→ Σ ⟷ (∀n. ∃n0. ∀k≥n0. σ k ∈ ℬ↓(Σ, n))›
  by (metis restriction_cball_mem_iff restriction_tendsto_def)

corollary restriction_tendsto_restriction_cballI : ‹(⋀n. ∃n0. ∀k≥n0. σ k ∈ ℬ↓(Σ, n)) ⟹ σ ─↓→ Σ›
  by (simp add: restriction_tendsto_iff_restriction_cball_characterization)

corollary restriction_tendsto_restriction_cballD : ‹σ ─↓→ Σ ⟹ ∃n0. ∀k≥n0. σ k ∈ ℬ↓(Σ, n)›
  by (simp add: restriction_tendsto_iff_restriction_cball_characterization)

corollary restriction_tendsto_restriction_cballE :
  ‹σ ─↓→ Σ ⟹ (⋀n0. (⋀k. n0 ≤ k ⟹ σ k ∈ ℬ↓(Σ, n)) ⟹ thesis) ⟹ thesis›
  using restriction_tendsto_restriction_cballD by blast

end



context restriction begin

theorem restriction_closed_iff_sequential_characterization :
  ‹closed↓ S ⟷ (∀Σ σ. range σ ⊆ S ⟶ σ ─↓→ Σ ⟶ Σ ∈ S)›
proof (intro iffI allI impI)
  show ‹restriction_closed S ⟹ range σ ⊆ S ⟹ σ ─↓→ Σ ⟹ Σ ∈ S› for Σ σ
    by (meson le_add1 range_subsetD restriction_closedD)
next
  assume * : ‹∀Σ σ. range σ ⊆ S ⟶ σ ─↓→ Σ ⟶ Σ ∈ S›
  show ‹closed↓ S›
  proof (rule restriction_closedI, rule ccontr)
    fix Σ σ assume ‹Σ ∉ S› ‹σ ─↓→ Σ› ‹∄n0. ∀k≥n0. σ k ∉ S›
    from ‹∄n0. ∀k≥n0. σ k ∉ S› INFM_nat_le have ‹∃∞k. σ k ∈ S› by auto
    from this[THEN extraction_subseqD[of ‹λx. x ∈ S›]]
    obtain f :: ‹nat ⇒ nat› where ‹strict_mono f› ‹∀k. σ (f k) ∈ S› by blast
    from ‹∀k. σ (f k) ∈ S› have ‹range (σ ∘ f) ⊆ S› by auto
    moreover from ‹strict_mono f› ‹σ ─↓→ Σ› have ‹(σ ∘ f) ─↓→ Σ›
      by (fact restriction_tendsto_subseq)
    ultimately have ‹Σ ∈ S› by (fact "*"[rule_format])
    with ‹Σ ∉ S› show False ..
  qed
qed


corollary restriction_closed_sequentialI :
  ‹(⋀Σ σ. range σ ⊆ S ⟹ σ ─↓→ Σ ⟹ Σ ∈ S) ⟹ closed↓ S›
  by (simp add: restriction_closed_iff_sequential_characterization)

corollary restriction_closed_sequentialD :
  ‹closed↓ S ⟹ range σ ⊆ S ⟹ σ ─↓→ Σ ⟹ Σ ∈ S›
  by (simp add: restriction_closed_iff_sequential_characterization)

end



context restriction_space begin

theorem restriction_open_iff_restriction_cball_characterization :
  ‹open↓ U ⟷ (∀Σ∈U. ∃n. ℬ↓(Σ, n) ⊆ U)›
proof (intro iffI ballI)
  show ‹open↓ U ⟹ Σ ∈ U ⟹ ∃n. ℬ↓(Σ, n) ⊆ U› for Σ
  proof (rule ccontr)
    assume ‹open↓ U› ‹Σ ∈ U› ‹∄n. ℬ↓(Σ, n) ⊆ U›
    from ‹∄n. ℬ↓(Σ, n) ⊆ U› have ‹∀n. ∃σ. σ ∈ ℬ↓(Σ, n) ∩ - U› by auto
    then obtain σ where ‹σ n ∈ ℬ↓(Σ, n)› ‹σ n ∈ - U› for n by (metis IntE)
    from ‹⋀n. σ n ∈ ℬ↓(Σ, n)› have ‹σ ─↓→ Σ› 
      by (metis restriction_cball_memD restriction_related_le restriction_tendstoI)
    moreover from ‹open↓ U› have ‹closed↓ (- U)›
      by (simp add: restriction_closed_def)
    ultimately have ‹Σ ∈ - U›
      using ‹⋀n. σ n ∈ - U› restriction_closedD by blast
    with ‹Σ ∈ U› show False by simp
  qed
next
  show ‹∀Σ∈U. ∃n. ℬ↓(Σ, n) ⊆ U ⟹ open↓ U›
    by (metis center_mem_restriction_cball restriction_open_def
        restriction_open_restriction_cball subset_iff)
qed


corollary restriction_open_restriction_cballI :
  ‹(⋀Σ. Σ ∈ U ⟹ ∃n. ℬ↓(Σ, n) ⊆ U) ⟹ open↓ U›
  by (simp add: restriction_open_iff_restriction_cball_characterization)

corollary restriction_open_restriction_cballD :
  ‹open↓ U ⟹ Σ ∈ U ⟹ ∃n. ℬ↓(Σ, n) ⊆ U›
  by (simp add: restriction_open_iff_restriction_cball_characterization)

corollary restriction_open_restriction_cballE :
  ‹open↓ U ⟹ Σ ∈ U ⟹ (⋀n. ℬ↓(Σ, n) ⊆ U ⟹ thesis) ⟹ thesis›
  using restriction_open_restriction_cballD by blast

end


context restriction begin

definition restriction_cont_on :: ‹['b :: restriction ⇒ 'a, 'b set] ⇒ bool›
  (‹cont↓ (_) on (_)› [1000, 1000])
  where ‹cont↓ f on A ≡ ∀Σ∈A. cont↓ f at Σ›

lemma restriction_cont_onI : ‹(⋀Σ σ. Σ ∈ A ⟹ σ ─↓→ Σ ⟹ (λn. f (σ n)) ─↓→ f Σ) ⟹ cont↓ f on A›
  by (simp add: restriction_cont_on_def restriction_cont_atI)

lemma restriction_cont_onD : ‹cont↓ f on A ⟹ Σ ∈ A ⟹ σ ─↓→ Σ ⟹ (λn. f (σ n)) ─↓→ f Σ›
  by (simp add: restriction_cont_on_def restriction_cont_atD)

lemma restriction_cont_on_comp [restriction_cont_simpset] :
  ‹cont↓ f on A ⟹ cont↓ g on B ⟹ f ` A ⊆ B ⟹ cont↓ (λx. g (f x)) on A›
  by (simp add: image_subset_iff restriction_cont_at_comp
      restriction_cont_on_def restriction_class.restriction_cont_on_def)

lemma restriction_cont_on_if_then_else [restriction_cont_simpset] :
  ‹⟦⋀x. P x ⟹ cont↓ (f x) on A; ⋀x. ¬ P x ⟹ cont↓ (g x) on A⟧
   ⟹ cont↓ (λy. if P x then f x y else g x y) on A›
  by (auto intro!: restriction_cont_onI) (blast dest: restriction_cont_onD)+

lemma restriction_cont_on_subset [restriction_cont_simpset] :
  ‹cont↓ f on B ⟹ A ⊆ B ⟹ cont↓ f on A›
  by (simp add: restriction_cont_on_def subset_iff)


abbreviation restriction_cont :: ‹['b :: restriction ⇒ 'a] ⇒ bool› (‹cont↓›)
  where ‹cont↓ f ≡ cont↓ f on UNIV›

lemma restriction_contI : ‹(⋀Σ σ. σ ─↓→ Σ ⟹ (λn. f (σ n)) ─↓→ f Σ) ⟹ cont↓ f›
  by (simp add: restriction_cont_onI)

lemma restriction_contD : ‹cont↓ f ⟹ σ ─↓→ Σ ⟹ (λn. f (σ n)) ─↓→ f Σ›
  by (simp add: restriction_cont_onD)

lemma restriction_cont_comp [restriction_cont_simpset] :
  ‹cont↓ g ⟹ cont↓ f ⟹ cont↓ (λx. g (f x))›
  by (simp add: restriction_cont_on_comp)

lemma restriction_cont_if_then_else [restriction_cont_simpset] :
  ‹⟦⋀x. P x ⟹ cont↓ (f x); ⋀x. ¬ P x ⟹ cont↓ (g x)⟧
   ⟹ cont↓ (λy. if P x then f x y else g x y)›
  by (auto intro!: restriction_contI) (blast dest: restriction_contD)+

end



context restriction_space begin

theorem restriction_cont_at_iff_restriction_cball_characterization :
  ‹cont↓ f at Σ ⟷ (∀n. ∃k. f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n))›
  for f :: ‹'b :: restriction_space ⇒ 'a›
proof (intro iffI allI)
  show ‹∃k. f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n)› if ‹cont↓ f at Σ› for n
  proof (rule ccontr)
    assume ‹∄k. f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n)›
    hence ‹∀k. ∃ψ. ψ ∈ f ` ℬ↓(Σ, k) ∧ ψ ∉ ℬ↓(f Σ, n)› by auto
    then obtain ψ where * : ‹ψ k ∈ f ` ℬ↓(Σ, k)› ‹ψ k ∉ ℬ↓(f Σ, n)› for k by metis
    from "*"(1) obtain σ where ** : ‹σ k ∈ ℬ↓(Σ, k)› ‹ψ k = f (σ k)› for k
      by (simp add: image_iff) metis
    have ‹σ ─↓→ Σ›
      by (rule restriction_class.restriction_tendsto_restriction_cballI)
        (use "**"(1) restriction_space_class.restriction_cball_anti_mono in blast)
    with restriction_cont_atD ‹restriction_cont_at f Σ›
    have ‹(λk. f (σ k)) ─↓→ f Σ› by blast
    hence ‹ψ ─↓→ f Σ› by (fold "**"(2))
    with "*"(2) restriction_tendsto_restriction_cballD show False by blast
  qed
next
  show ‹∀n. ∃k. f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n) ⟹ cont↓ f at Σ›
    by (intro restriction_cont_atI restriction_tendsto_restriction_cballI)
      (meson image_iff restriction_class.restriction_tendsto_restriction_cballD subset_eq)
qed


corollary restriction_cont_at_restriction_cballI :
  ‹(⋀n. ∃k. f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n)) ⟹ cont↓ f at Σ›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  by (simp add: restriction_cont_at_iff_restriction_cball_characterization)

corollary restriction_cont_at_restriction_cballD :
  ‹cont↓ f at Σ ⟹ ∃k. f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n)›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  by (simp add: restriction_cont_at_iff_restriction_cball_characterization)

corollary restriction_cont_at_restriction_cballE :
  ‹cont↓ f at Σ ⟹ (⋀k. f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n) ⟹ thesis) ⟹ thesis›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  using restriction_cont_at_restriction_cballD by blast



theorem restriction_cont_iff_restriction_open_characterization :
  ‹cont↓ f ⟷ (∀U. open↓ U ⟶ open↓ (f -` U))›
  for f :: ‹'b :: restriction_space ⇒ 'a›
proof (intro iffI allI impI)
  fix U :: ‹'a set› assume ‹cont↓ f› ‹open↓ U›
  show ‹open↓ (f -` U)›
  proof (rule restriction_space_class.restriction_open_restriction_cballI)
    fix Σ assume ‹Σ ∈ f -` U›
    hence ‹f Σ ∈ U› by simp
    with ‹open↓ U› restriction_open_restriction_cballD
    obtain n where ‹ℬ↓(f Σ, n) ⊆ U› by blast
    moreover obtain k where ‹f ` ℬ↓(Σ, k) ⊆ ℬ↓(f Σ, n)›
      by (meson UNIV_I ‹cont↓ f› restriction_cont_at_restriction_cballE restriction_cont_on_def)
    ultimately have ‹ℬ↓(Σ, k) ⊆ f -` U› by blast
    thus ‹∃k. ℬ↓(Σ, k) ⊆ f -` U› ..
  qed
next
  show ‹∀U. open↓ U ⟶ open↓ (f -` U) ⟹ cont↓ f›
    by (unfold restriction_cont_on_def, intro ballI restriction_cont_at_restriction_cballI)
      (simp add: image_subset_iff_subset_vimage restriction_space_class.restriction_open_restriction_cballD)
qed

corollary restriction_cont_restriction_openI :
  ‹(⋀U. open↓ U ⟹ open↓ (f -` U)) ⟹ cont↓ f›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  by (simp add: restriction_cont_iff_restriction_open_characterization)

corollary restriction_cont_restriction_openD :
  ‹cont↓ f ⟹ open↓ U ⟹ open↓ (f -` U)›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  by (simp add: restriction_cont_iff_restriction_open_characterization)


theorem restriction_cont_iff_restriction_closed_characterization :
  ‹cont↓ f ⟷ (∀S. closed↓ S ⟶ closed↓ (f -` S))›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  by (metis boolean_algebra_class.boolean_algebra.double_compl local.restriction_closed_def
      restriction_class.restriction_closed_def restriction_cont_iff_restriction_open_characterization vimage_Compl)

corollary restriction_cont_restriction_closedI :
  ‹(⋀U. closed↓ U ⟹ closed↓ (f -` U)) ⟹ cont↓ f›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  by (simp add: restriction_cont_iff_restriction_closed_characterization)

corollary restriction_cont_restriction_closedD :
  ‹cont↓ f ⟹ closed↓ U ⟹ closed↓ (f -` U)›
  for f :: ‹'b :: restriction_space ⇒ 'a›
  by (simp add: restriction_cont_iff_restriction_closed_characterization)


theorem restriction_shift_on_restriction_open_imp_restriction_cont_on :
  ‹cont↓ f on U› if ‹open↓ U› and ‹restriction_shift_on f k U›
proof (intro restriction_cont_onI restriction_tendstoI)
  fix Σ σ and n :: nat assume ‹Σ ∈ U› ‹σ ─↓→ Σ›
  with ‹open↓ U› obtain n0 where ‹∀l≥n0. σ l ∈ U›
    by (meson restriction_class.restriction_openD)
  moreover from ‹σ ─↓→ Σ›[THEN restriction_class.restriction_tendstoD]
  obtain n1 where ‹∀l≥n1. Σ ↓ nat (int n - k) = σ l ↓ nat (int n - k)› ..
  ultimately have ‹∀l≥max n0 n1. σ l ∈ U ∧ Σ ↓ nat (int n - k) = σ l ↓ nat (int n - k)› by simp
  with ‹Σ ∈ U› ‹restriction_shift_on f k U› restriction_shift_onD
  have ‹∀l≥max n0 n1. f Σ ↓ nat (int (nat (int n - k)) + k) = f (σ l) ↓ nat (int (nat (int n - k)) + k)› by blast
  moreover have ‹n ≤ nat (int (nat (int n - k)) + k)› by auto
  ultimately have ‹∀l≥max n0 n1. f Σ ↓ n = f (σ l) ↓ n› by (meson restriction_related_le)
  thus ‹∃n2. ∀l≥n2. f Σ ↓ n = f (σ l) ↓ n› by blast
qed

corollary restriction_shift_imp_restriction_cont [restriction_cont_simpset] :
  ‹restriction_shift f k ⟹ cont↓ f›
  by (simp add: restriction_shift_def
      restriction_shift_on_restriction_open_imp_restriction_cont_on)

corollary non_too_destructive_imp_restriction_cont [restriction_cont_simpset] :
  ‹non_too_destructive f ⟹ cont↓ f›
  by (simp add: non_too_destructive_def non_too_destructive_on_def
      restriction_shift_on_restriction_open_imp_restriction_cont_on)


end



subsection ‹Compactness›

context restriction begin

definition restriction_compact :: ‹'a set ⇒ bool› (‹compact↓›)
  where ‹compact↓ K ≡
         ∀σ. range σ ⊆ K ⟶
         (∃f :: nat ⇒ nat. ∃Σ. Σ ∈ K ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ)›


lemma restriction_compactI :
  ‹(⋀σ. range σ ⊆ K ⟹ ∃f :: nat ⇒ nat. ∃Σ. Σ ∈ K ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ)
   ⟹ compact↓ K› by (simp add: restriction_compact_def)

lemma restriction_compactD :
  ‹compact↓ K ⟹ range σ ⊆ K ⟹
   ∃f :: nat ⇒ nat. ∃Σ. Σ ∈ K ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ›
  by (simp add: restriction_compact_def)

lemma restriction_compactE :
  assumes ‹compact↓ K› and ‹range σ ⊆ K›
  obtains f :: ‹nat ⇒ nat› and Σ where ‹Σ ∈ K› ‹strict_mono f› ‹(σ ∘ f) ─↓→ Σ›
  by (meson assms restriction_compactD)

lemma restriction_compact_empty [simp] : ‹compact↓ {}›
  by (simp add: restriction_compact_def)



lemma (in restriction_space) restriction_compact_imp_restriction_closed :
  ‹closed↓ K› if ‹compact↓ K›
proof (rule restriction_closed_sequentialI)
  fix σ Σ assume ‹range σ ⊆ K› ‹σ ─↓→ Σ›
  from restriction_compactD ‹compact↓ K› ‹range σ ⊆ K› 
  obtain f and Σ' where ‹Σ' ∈ K› ‹strict_mono f› ‹(σ ∘ f) ─↓→ Σ'› by blast
  from restriction_tendsto_subseq ‹strict_mono f› ‹σ ─↓→ Σ›
  have ‹(σ ∘ f) ─↓→ Σ› by blast
  with ‹(σ ∘ f) ─↓→ Σ'› have ‹Σ' = Σ› by (fact restriction_tendsto_unique)
  with ‹Σ' ∈ K› show ‹Σ ∈ K› by simp
qed


lemma restriction_compact_union : ‹compact↓ (K ∪ L)›
  if ‹compact↓ K› and ‹compact↓ L›
proof (rule restriction_compactI)
  fix σ :: ‹nat ⇒ _› assume ‹range σ ⊆ K ∪ L›
  { fix K L and f :: ‹nat ⇒ nat›
    assume ‹compact↓ K› ‹strict_mono f› ‹σ (f n) ∈ K› for n
    from ‹(⋀n. σ (f n) ∈ K)› have ‹range (σ ∘ f) ⊆ K› by auto
    with ‹compact↓ K› restriction_compactD obtain g Σ
      where ‹Σ ∈ K› ‹strict_mono g› ‹(σ ∘ f ∘ g) ─↓→ Σ› by blast
    hence ‹Σ ∈ K ∪ L ∧ strict_mono (f ∘ g) ∧ (σ ∘ (f ∘ g)) ─↓→ Σ›
      by (metis (no_types, lifting) Un_iff ‹strict_mono f› comp_assoc
          monotone_on_o subset_UNIV)
    hence ‹∃f Σ. Σ ∈ K ∪ L ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ› by blast
  } note * = this
  have ‹(∃∞n. σ n ∈ K) ∨ (∃∞n. σ n ∈ L)›
  proof (rule ccontr)
    assume ‹¬ ((∃∞n. σ n ∈ K) ∨ (∃∞n. σ n ∈ L))›
    hence ‹finite {n. σ n ∈ K} ∧ finite {n. σ n ∈ L}›
      using frequently_cofinite by blast
    then obtain n where ‹n ∉ {n. σ n ∈ K} ∧ n ∉ {n. σ n ∈ L}›
      by (metis (mono_tags, lifting) INFM_nat_le dual_order.refl
          frequently_cofinite le_sup_iff mem_Collect_eq)
    hence ‹σ n ∉ K ∪ L› by simp
    with ‹range σ ⊆ K ∪ L› show False by blast
  qed
  thus ‹∃f Σ. Σ ∈ K ∪ L ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ›
    by (elim disjE extraction_subseqE)
      (use "*" ‹compact↓ K› in blast, metis "*" Un_iff ‹compact↓ L›)
qed

lemma restriction_compact_finite_Union :
  ‹⟦finite I; ⋀i. i ∈ I ⟹ compact↓ (K i)⟧ ⟹ compact↓ (⋃i∈I. K i)›
  by (induct I rule: finite_induct)
    (simp_all add: restriction_compact_union)


lemma (in restriction_space) restriction_compact_Inter :
  ‹compact↓ (⋂i. K i)› if ‹⋀i. compact↓ (K i)›
proof (rule restriction_compactI)
  fix σ :: ‹nat ⇒ 'a› assume ‹range σ ⊆ ⋂ (range K)›
  hence ‹range σ ⊆ K i› for i by blast
  with ‹⋀i. compact↓ (K i)› restriction_compactD
  obtain f Σ where ‹strict_mono f› ‹(σ ∘ f) ─↓→ Σ› by blast
  from ‹⋀i. compact↓ (K i)› have ‹closed↓ (K i)› for i
    by (simp add: restriction_compact_imp_restriction_closed)
  moreover from ‹⋀i. range σ ⊆ K i› have ‹range (σ ∘ f) ⊆ K i› for i by auto
  ultimately have ‹Σ ∈ K i› for i
    by (meson ‹(σ ∘ f) ─↓→ Σ› restriction_closed_sequentialD)
  with ‹strict_mono f› ‹(σ ∘ f) ─↓→ Σ›
  show ‹∃f Σ. Σ ∈ ⋂ (range K) ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ› by blast
qed

lemma finite_imp_restriction_compact : ‹compact↓ K› if ‹finite K›
proof (rule restriction_compactI)
  fix σ :: ‹nat ⇒ _› assume ‹range σ ⊆ K›
  have ‹∃Σ∈K. ∃∞n. σ n = Σ›
  proof (rule ccontr)
    assume ‹¬ (∃Σ∈K. ∃∞n. σ n = Σ)›
    hence ‹∀Σ∈K. finite {n. σ n = Σ}› by (simp add: frequently_cofinite)
    with ‹finite K› have ‹finite (⋃Σ∈K. {n. σ n = Σ})› by blast
    also from ‹range σ ⊆ K› have ‹(⋃Σ∈K. {n. σ n = Σ}) = UNIV› by auto
    finally show False by simp
  qed
  then obtain Σ where ‹Σ ∈ K› ‹∃∞n. σ n = Σ› ..
  from extraction_subseqD[of _ σ, OF ‹∃∞n. σ n = Σ›]
  obtain f :: ‹nat ⇒ nat› where ‹strict_mono f› ‹σ (f n) = Σ› for n by blast
  from ‹⋀n. σ (f n) = Σ› have ‹(σ ∘ f) ─↓→ Σ›
    by (simp add: restriction_tendstoI)
  with ‹strict_mono f› ‹Σ ∈ K›
  show ‹∃f Σ. Σ ∈ K ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ› by blast
qed


lemma restriction_compact_restriction_closed_subset : ‹compact↓ L›
  if ‹L ⊆ K› ‹compact↓ K› ‹closed↓ L›
proof (rule restriction_compactI)
  fix σ :: ‹nat ⇒ _› assume ‹range σ ⊆ L›
  with ‹L ⊆ K› have ‹range σ ⊆ K› by blast
  with ‹compact↓ K› restriction_compactD
  obtain f Σ where ‹Σ ∈ K› ‹strict_mono f› ‹(σ ∘ f) ─↓→ Σ› by blast
  from ‹range σ ⊆ L› have ‹range (σ ∘ f) ⊆ L› by auto
  from restriction_closed_sequentialD ‹restriction_closed L›
    ‹(σ ∘ f) ─↓→ Σ› ‹range (σ ∘ f) ⊆ L› have ‹Σ ∈ L› by blast
  with ‹strict_mono f› ‹(σ ∘ f) ─↓→ Σ›
  show ‹∃f Σ. Σ ∈ L ∧ strict_mono f ∧ (σ ∘ f) ─↓→ Σ› by blast
qed


lemma restriction_cont_image_of_restriction_compact :
  ‹compact↓ (f ` K)› if ‹compact↓ K› and ‹cont↓ f on K›
proof (rule restriction_compactI)
  fix σ :: ‹nat ⇒ _› assume ‹range σ ⊆ f ` K›
  hence ‹∀n. ∃γ. γ ∈ K ∧ σ n = f γ› by (meson imageE range_subsetD)
  then obtain γ :: ‹nat ⇒ _› where ‹range γ ⊆ K› ‹σ n = f (γ n)› for n
    by (metis image_subsetI)
  from restriction_class.restriction_compactD[OF ‹compact↓ K› ‹range γ ⊆ K›]
  obtain g Σ where ‹Σ ∈ K› ‹strict_mono g› ‹(γ ∘ g) ─↓→ Σ› by blast
  from ‹cont↓ f on K› ‹Σ ∈ K›
  have ‹cont↓ f at Σ› by (simp add: restriction_cont_on_def)
  with ‹(γ ∘ g) ─↓→ Σ› restriction_cont_atD
  have ‹(λn. f ((γ ∘ g) n)) ─↓→ f Σ› by blast 
  also have ‹(λn. f ((γ ∘ g) n)) = (σ ∘ g)›
    by (simp add: ‹⋀n. σ n = f (γ n)› comp_def)
  finally have ‹(σ ∘ g) ─↓→ f Σ› .
  with ‹Σ ∈ K› ‹strict_mono g›
  show ‹∃g Σ. Σ ∈ f ` K ∧ strict_mono g ∧ (σ ∘ g) ─↓→ Σ› by blast
qed

end





subsection ‹Properties for Function and Product›

lemma restriction_cball_fun_is : ‹ℬ↓(f, n) = {g. ∀x. g x ∈ ℬ↓(f x, n)}›
  by (simp add: set_eq_iff restriction_cball_mem_iff restriction_fun_def) metis

lemma restriction_cball_prod_is :
  ‹ℬ↓(Σ, n) = ℬ↓(fst Σ, n) × ℬ↓(snd Σ, n)›
  by (simp add: set_eq_iff restriction_cball_def restriction_prod_def)


lemma restriction_open_prod_imp_restriction_open_image_fst :
  ‹open↓ (fst ` U)› if ‹open↓ U›
proof (rule restriction_openI)
  fix Σ σ assume ‹Σ ∈ fst ` U› and ‹σ ─↓→ Σ›
  from ‹Σ ∈ fst ` U› obtain v where ‹(Σ, v) ∈ U› by auto
  from ‹σ ─↓→ Σ› have ‹(λn. (σ n, v)) ─↓→ (Σ, v)›
    by (simp add: restriction_tendsto_prod_iff restriction_tendsto_const)
  from restriction_openD[OF ‹restriction_open U› ‹(Σ, v) ∈ U› this]
  obtain n0 where ‹∀k≥n0. (σ k, v) ∈ U› ..
  thus ‹∃n0. ∀k≥n0. σ k ∈ fst ` U› by (metis fst_conv imageI)
qed

lemma restriction_open_prod_imp_restriction_open_image_snd :
  ‹open↓ (snd ` U)› if ‹open↓ U›
proof (rule restriction_openI)
  fix Σ σ assume ‹Σ ∈ snd ` U› and ‹σ ─↓→ Σ›
  from ‹Σ ∈ snd ` U› obtain u where ‹(u, Σ) ∈ U› by auto
  from ‹σ ─↓→ Σ› have ‹(λn. (u, σ n)) ─↓→ (u, Σ)›
    by (simp add: restriction_tendsto_prod_iff restriction_tendsto_const)
  from restriction_openD[OF ‹restriction_open U› ‹(u, Σ) ∈ U› this]
  obtain n0 where ‹∀k≥n0. (u, σ k) ∈ U› ..
  thus ‹∃n0. ∀k≥n0. σ k ∈ snd ` U› by (metis snd_conv imageI)
qed

lemma restriction_open_prod_iff :
  ‹open↓ (U × V) ⟷ (V = {} ∨ open↓ U) ∧ (U = {} ∨ open↓ V)›
proof (intro iffI conjI)
  show ‹open↓ (U × V) ⟹ V = {} ∨ open↓ U›
    by (metis fst_image_times restriction_open_prod_imp_restriction_open_image_fst)
next
  show ‹open↓ (U × V) ⟹ U = {} ∨ open↓ V›
    by (metis restriction_open_prod_imp_restriction_open_image_snd snd_image_times)
next
  assume ‹(V = {} ∨ open↓ U) ∧ (U = {} ∨ open↓ V)›
  then consider ‹U = {}› | ‹V = {}› | ‹open↓ U ∧ open↓ V› by fast
  thus ‹open↓ (U × V)›
  proof cases
    show ‹U = {} ⟹ open↓ (U × V)› by simp
  next
    show ‹V = {} ⟹ open↓ (U × V)› by simp
  next
    show ‹open↓ (U × V)› if * : ‹open↓ U ∧ open↓ V›
    proof (rule restriction_openI)
      fix Σ σ assume ‹Σ ∈ U × V› and ‹σ ─↓→ Σ›
      from ‹Σ ∈ U × V› have ‹fst Σ ∈ U› ‹snd Σ ∈ V› by auto
      from ‹σ ─↓→ Σ› have ‹(λn. fst (σ n)) ─↓→ fst Σ› ‹(λn. snd (σ n)) ─↓→ snd Σ›
        by (simp_all add: restriction_tendsto_prod_iff)
      from restriction_openD[OF "*"[THEN conjunct1] ‹fst Σ ∈ U› ‹(λn. fst (σ n)) ─↓→ fst Σ›]
      obtain n0 where ‹∀k≥n0. fst (σ k) ∈ U› ..
      moreover from restriction_openD[OF "*"[THEN conjunct2] ‹snd Σ ∈ V› ‹(λn. snd (σ n)) ─↓→ snd Σ›]
      obtain n1 where ‹∀k≥n1. snd (σ k) ∈ V› ..
      ultimately have ‹∀k≥max n0 n1. σ k ∈ U × V› by (simp add: mem_Times_iff)
      thus ‹∃n2. ∀k≥n2. σ k ∈ U × V› by blast
    qed
  qed
qed



lemma restriction_cont_at_prod_codomain_iff:
  ‹cont↓ f at Σ ⟷ cont↓ (λx. fst (f x)) at Σ ∧ cont↓ (λx. snd (f x)) at Σ›
  by (auto simp add: restriction_cont_at_def restriction_tendsto_prod_iff)

lemma restriction_cont_on_prod_codomain_iff:
  ‹cont↓ f on A ⟷ cont↓ (λx. fst (f x)) on A ∧ cont↓ (λx. snd (f x)) on A›
  by (metis restriction_cont_at_prod_codomain_iff restriction_cont_on_def)

lemma restriction_cont_prod_codomain_iff:
  ‹cont↓ f ⟷ cont↓ (λx. fst (f x)) ∧ cont↓ (λx. snd (f x))›
  by (fact restriction_cont_on_prod_codomain_iff)


lemma restriction_cont_at_prod_codomain_imp [restriction_cont_simpset] :
  ‹cont↓ f at Σ ⟹ cont↓ (λx. fst (f x)) at Σ›
  ‹cont↓ f at Σ ⟹ cont↓ (λx. snd (f x)) at Σ›
  by (simp_all add: restriction_cont_at_prod_codomain_iff)

lemma restriction_cont_on_prod_codomain_imp [restriction_cont_simpset] :
  ‹cont↓ f on A ⟹ cont↓ (λx. fst (f x)) on A›
  ‹cont↓ f on A ⟹ cont↓ (λx. snd (f x)) on A›
  by (simp_all add: restriction_cont_on_prod_codomain_iff)

lemma restriction_cont_prod_codomain_imp [restriction_cont_simpset] :
  ‹cont↓ f ⟹ cont↓ (λx. fst (f x))›
  ‹cont↓ f ⟹ cont↓ (λx. snd (f x))›
  by (simp_all add: restriction_cont_prod_codomain_iff)




lemma restriction_cont_at_fun_imp [restriction_cont_simpset] :
  ‹cont↓ f at A ⟹ cont↓ (λx. f x y) at A›
  by (rule restriction_cont_atI)
    (metis restriction_cont_atD restriction_tendsto_fun_imp)

lemma restriction_cont_on_fun_imp [restriction_cont_simpset] :
  ‹cont↓ f on A ⟹ cont↓ (λx. f x y) on A›
  by (simp add: restriction_cont_at_fun_imp restriction_cont_on_def)

corollary restriction_cont_fun_imp [restriction_cont_simpset] :
  ‹cont↓ f ⟹ cont↓ (λx. f x y)›
  by (fact restriction_cont_on_fun_imp) 



lemma restriction_cont_at_prod_domain_imp [restriction_cont_simpset] :
  ‹cont↓ f at Σ ⟹ cont↓ (λx. f (x, snd Σ)) at (fst Σ)›
  ‹cont↓ f at Σ ⟹ cont↓ (λy. f (fst Σ, y)) at (snd Σ)›
  for f :: ‹'a :: restriction_space × 'b :: restriction_space ⇒ 'c :: restriction_space›
  by (simp add: restriction_cball_prod_is subset_iff image_iff
      restriction_cont_at_iff_restriction_cball_characterization,
      meson center_mem_restriction_cball)+

lemma restriction_cont_on_prod_domain_imp [restriction_cont_simpset] :
  ‹cont↓ (λx. f (x, y)) on {x. (x, y) ∈ A}›
  ‹cont↓ (λy. f (x, y)) on {y. (x, y) ∈ A}› if ‹cont↓ f on A›
for f :: ‹'a :: restriction_space × 'b :: restriction_space ⇒ 'c :: restriction_space›
proof -
  show ‹cont↓ (λx. f (x, y)) on {x. (x, y) ∈ A}›
  proof (unfold restriction_cont_on_def, rule ballI)
    fix x assume ‹x ∈ {x. (x, y) ∈ A}›
    with ‹cont↓ f on A› have ‹cont↓ f at (x, y)›
      unfolding restriction_cont_on_def by simp
    thus ‹cont↓ (λx. f (x, y)) at x›
      by (fact restriction_cont_at_prod_domain_imp[of f ‹(x, y)›, simplified])
  qed
next
  show ‹cont↓ (λy. f (x, y)) on {y. (x, y) ∈ A}›
  proof (unfold restriction_cont_on_def, rule ballI)
    fix y assume ‹y ∈ {y. (x, y) ∈ A}›
    with ‹cont↓ f on A› have ‹cont↓ f at (x, y)›
      unfolding restriction_cont_on_def by simp
    thus ‹cont↓ (λy. f (x, y)) at y›
      by (fact restriction_cont_at_prod_domain_imp[of f ‹(x, y)›, simplified])
  qed
qed

lemma restriction_cont_prod_domain_imp [restriction_cont_simpset] :
  ‹cont↓ f ⟹ cont↓ (λx. f (x, y))›
  ‹cont↓ f ⟹ cont↓ (λy. f (x, y))›
for f :: ‹'a :: restriction_space × 'b :: restriction_space ⇒ 'c :: restriction_space›
  by (metis UNIV_I restriction_cont_at_prod_domain_imp(1) restriction_cont_on_def split_pairs)
    (metis UNIV_I restriction_cont_at_prod_domain_imp(2) restriction_cont_on_def split_pairs)



(*<*)
end
  (*>*)