Theory Urysohn_Locally_Compact_Hausdorff

(*  Title:   Urysohn_Locally_Compact_Hausdorff.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

section  ‹Urysohn's Lemma ›
theory Urysohn_Locally_Compact_Hausdorff
  imports "Standard_Borel_Spaces.StandardBorel"
begin

text ‹ We prove Urysohn's lemma for locally compact Hausdorff space (Lemma 2.12~\cite{Rudin}) ›

subsection ‹ Lemmas for Upper/Lower Semi-Continuous Functions ›
lemma 
  assumes "⋀x. x ∈ topspace X ⟹ f x = g x"
  shows upper_semicontinuous_map_cong:
    "upper_semicontinuous_map X f ⟷ upper_semicontinuous_map X g" (is ?g1)
    and lower_semicontinuous_map_cong:
    "lower_semicontinuous_map X f ⟷ lower_semicontinuous_map X g" (is ?g2)
proof -
  have [simp]:"⋀a. {x∈topspace X. f x < a} = {x∈topspace X. g x < a}"
              "⋀a. {x∈topspace X. f x > a} = {x∈topspace X. g x > a}"
    using assms by auto
  show ?g1 ?g2
    by(auto simp: upper_semicontinuous_map_def lower_semicontinuous_map_def)
qed

lemma upper_lower_semicontinuous_map_iff_continuous_map:
  "continuous_map X euclidean f ⟷ upper_semicontinuous_map X f ∧ lower_semicontinuous_map X f"
  using continuous_map_upper_lower_semicontinuous_lt
        lower_semicontinuous_map_def upper_semicontinuous_map_def
  by blast

lemma [simp]:
  shows upper_semicontinuous_map_const: "upper_semicontinuous_map X (λx. c)"
    and lower_semicontinuous_map_const: "lower_semicontinuous_map X (λx. c)"
  using continuous_map_const[of _ euclidean c]
  unfolding upper_lower_semicontinuous_map_iff_continuous_map by auto

(* TODO: generalize the following with type classes *)
lemma upper_semicontinuous_map_c_add_iff:
  fixes c :: real
  shows "upper_semicontinuous_map X (λx. c + f x) ⟷ upper_semicontinuous_map X f"
proof -
  have [simp]: "c + f x < a ⟷ f x < a - c" for x a
    by auto
  show ?thesis
    by(simp add: upper_semicontinuous_map_def) (metis add_diff_cancel_left')
qed

corollary upper_semicontinuous_map_add_c_iff:
  fixes c :: real
  shows "upper_semicontinuous_map X (λx. f x + c) ⟷ upper_semicontinuous_map X f"
  by(simp add: add.commute upper_semicontinuous_map_c_add_iff)
(* TODO: end *)

lemma upper_semicontinuous_map_posreal_cmult_iff:
  fixes c :: real
  assumes "c > 0"
  shows "upper_semicontinuous_map X (λx. c * f x) ⟷ upper_semicontinuous_map X f"
proof -
  have [simp]: "c * f x < a ⟷ f x < a / c" for x a
    using assms by (simp add: less_divide_eq mult.commute)
  thus ?thesis
    by(simp add: upper_semicontinuous_map_def)
      (metis assms less_numeral_extra(3) nonzero_mult_div_cancel_left)
qed

lemma upper_semicontinuous_map_real_cmult:
  fixes c :: real
  assumes "c ≥ 0" "upper_semicontinuous_map X f"
  shows "upper_semicontinuous_map X (λx. c * f x)"
  by(cases "c = 0")
    (use assms upper_semicontinuous_map_posreal_cmult_iff[simplified dual_order.strict_iff_order] in auto)

(* TODO: neg times *)
lemma lower_semicontinuous_map_posreal_cmult_iff:
  fixes c :: real
  assumes "c > 0"
  shows "lower_semicontinuous_map X (λx. c * f x) ⟷ lower_semicontinuous_map X f"
proof -
  have [simp]: "c * f x > a ⟷ f x > a / c" for x a
    by (simp add: assms divide_less_eq mult.commute)
  show ?thesis
    by(simp add: lower_semicontinuous_map_def)
      (metis assms less_numeral_extra(3) nonzero_mult_div_cancel_left)
qed

lemma lower_semicontinuous_map_real_cmult:
  fixes c :: real
  assumes "c ≥ 0" "lower_semicontinuous_map X f"
  shows "lower_semicontinuous_map X (λx. c * f x)"
  by(cases "c = 0")
    (use assms lower_semicontinuous_map_posreal_cmult_iff[simplified dual_order.strict_iff_order] in auto)

lemma upper_semicontinuous_map_INF:
  fixes f :: "_ ⇒ _ ⇒ 'a :: {linorder_topology, complete_linorder}"
  assumes "⋀i. i ∈ I ⟹  upper_semicontinuous_map X (f i)"
  shows "upper_semicontinuous_map X (λx. ⨅i∈I. f i x)"
  unfolding upper_semicontinuous_map_def
proof
  fix a
  have "{x ∈ topspace X. (⨅i∈I. f i x) < a} = (⋃i∈I. {x∈topspace X. f i x < a})"
    by(auto simp: Inf_less_iff)
  also have "openin X ..."
    using assms by(auto simp: upper_semicontinuous_map_def)
  finally show "openin X {x ∈ topspace X. (⨅i∈I. f i x) < a}" .
qed

lemma upper_semicontinuous_map_cInf:
  fixes f :: "_ ⇒ _ ⇒ 'a :: {linorder_topology, conditionally_complete_linorder}"
  assumes "I ≠ {}" "⋀x. x ∈ topspace X ⟹ bdd_below ((λi. f i x) ` I)"
      and "⋀i. i ∈ I ⟹  upper_semicontinuous_map X (f i)"
    shows "upper_semicontinuous_map X (λx. ⨅i∈I. f i x)"
  unfolding upper_semicontinuous_map_def
proof
  fix a
  have [simp]:"⋀x. x ∈ topspace X ⟹ (⨅i∈I. f i x) < a ⟷ (∃x∈(λi. f i x) ` I. x < a)"
    by(intro cInf_less_iff) (use assms in auto)
  have "{x ∈ topspace X. (⨅i∈I. f i x) < a} = (⋃i∈I. {x∈topspace X. f i x < a})"
    by auto
  also have "openin X ..."
    using assms by(auto simp: upper_semicontinuous_map_def)
  finally show "openin X {x ∈ topspace X. (⨅i∈I. f i x) < a}" .
qed

lemma lower_semicontinuous_map_Sup:
  fixes f :: "_ ⇒ _ ⇒ 'a :: {linorder_topology, complete_linorder}"
  assumes "⋀i. i ∈ I ⟹  lower_semicontinuous_map X (f i)"
  shows "lower_semicontinuous_map X (λx. ⨆i∈I. f i x)"
  unfolding lower_semicontinuous_map_def
proof
  fix a
  have "{x ∈ topspace X. (⨆i∈I. f i x) > a} = (⋃i∈I. {x∈topspace X. f i x > a})"
    by(auto simp: less_Sup_iff)
  also have "openin X ..."
    using assms by(auto simp: lower_semicontinuous_map_def)
  finally show "openin X {x ∈ topspace X. (⨆i∈I. f i x) > a}" .
qed

lemma indicator_closed_upper_semicontinuous_map:
  assumes "closedin X C"
  shows "upper_semicontinuous_map X (indicator C :: _ ⇒ 'a :: {zero_less_one, linorder_topology})"
  unfolding upper_semicontinuous_map_def
proof safe
  fix a :: 'a
  consider "a ≤ 0" | "0 < a" "a ≤ 1" | "1 < a"
    by fastforce
  then show "openin X {x ∈ topspace X. indicator C x < a}"
  proof cases
    case 1
    then have [simp]:"{x ∈ topspace X. indicator C x < a} = {}"
      by(simp add: indicator_def) (meson order.strict_iff_not order.trans zero_less_one_class.zero_le_one)
    show ?thesis
      by simp
  next
    case 2
    then have [simp]:"{x ∈ topspace X. indicator C x < a} = topspace X - C"
      by(fastforce simp add: indicator_def)
    show ?thesis
      using assms by auto
  next
    case 3
    then have [simp]: "{x ∈ topspace X. indicator C x < a} = topspace X"
      by (simp add: indicator_def dual_order.strict_trans2)
    show ?thesis
      by simp
  qed
qed

lemma indicator_open_lower_semicontinuous_map:
  assumes "openin X U"
  shows "lower_semicontinuous_map X (indicator U :: _ ⇒ 'a :: {zero_less_one, linorder_topology})"
  unfolding lower_semicontinuous_map_def
proof safe
  fix a :: 'a
  consider "a < 0" | "0 ≤ a" "a < 1" | "1 ≤ a"
    by fastforce
  then show "openin X {x ∈ topspace X. a < indicator U x}"
  proof cases
    case 1
    then have [simp]: "{x ∈ topspace X. a < indicator U x} = topspace X"
      using order_less_trans by (fastforce simp add: indicator_def )
    show ?thesis
      by simp
  next
    case 2
    then have [simp]:"{x ∈ topspace X. a < indicator U x} = U"
      using openin_subset[OF assms] by(simp add: indicator_def) fastforce
    show ?thesis
      by(simp add: assms)
  next
    case 3
    then have [simp]:"{x ∈ topspace X. a < indicator U x} = {}"
      by(simp add: indicator_def) (meson dual_order.strict_trans leD zero_less_one)
    show ?thesis
      by simp
  qed
qed

lemma lower_semicontinuous_map_cSup:
  fixes f :: "_ ⇒ _ ⇒ 'a :: {linorder_topology, conditionally_complete_linorder}"
  assumes "I ≠ {}" "⋀x. x ∈ topspace X ⟹ bdd_above ((λi. f i x) ` I)"
      and "⋀i. i ∈ I ⟹  lower_semicontinuous_map X (f i)"
  shows "lower_semicontinuous_map X (λx. ⨆i∈I. f i x)"
  unfolding lower_semicontinuous_map_def
proof
  fix a
  have [simp]:"⋀x. x ∈ topspace X ⟹ (⨆i∈I. f i x) > a ⟷ (∃x∈(λi. f i x) ` I. x > a)"
    by(intro less_cSup_iff) (use assms in auto)
  have "{x ∈ topspace X. (⨆i∈I. f i x) > a} = (⋃i∈I. {x∈topspace X. f i x > a})"
    by(auto simp: less_Sup_iff)
  also have "openin X ..."
    using assms by(auto simp: lower_semicontinuous_map_def)
  finally show "openin X {x ∈ topspace X. (⨆i∈I. f i x) > a}" .
qed

lemma openin_continuous_map_less:
  assumes "continuous_map X (euclidean :: ('a :: {dense_linorder, order_topology}) topology) f"
    and "continuous_map X euclidean g"
  shows "openin X {x∈topspace X. f x < g x}"
proof -
  have "{x∈topspace X. f x < g x} = {x∈topspace X. ∃r. f x < r ∧ r < g x}"
    using dense order.strict_trans by blast
  also have "... = (⋃r. {x∈topspace X. f x < r} ∩ {x∈topspace X. r < g x})"
    by blast
  also have "openin X ..."
    using assms by(fastforce simp: continuous_map_upper_lower_semicontinuous_lt)
  finally show ?thesis .
qed

corollary closedin_continuous_map_eq:
  assumes "continuous_map X (euclidean :: ('a :: {dense_linorder, order_topology}) topology) f"
    and "continuous_map X euclidean g"
  shows "closedin X {x∈topspace X. f x = g x}"
proof -
  have "{x∈topspace X. f x = g x} = topspace X - ({x∈topspace X. f x < g x} ∪ {x∈topspace X. f x > g x})"
    by auto
  also have "closedin X ..."
    using openin_continuous_map_less[OF assms] openin_continuous_map_less[OF assms(2,1)]
    by blast
  finally show ?thesis .
qed

subsection  ‹Urysohn's Lemma ›
lemma locally_compact_Hausdorff_compactin_openin_subset:
  assumes "locally_compact_space X" "Hausdorff_space X ∨ regular_space X"
      and "compactin X T" "openin X V" "T ⊆ V"
    shows "∃U. openin X U ∧ compactin X (X closure_of U) ∧ T ⊆ U ∧ (X closure_of U) ⊆ V"
proof -
  have "⋀x W. openin X W ⟹ x ∈ W
               ⟹ (∃U V. openin X U ∧ (compactin X V ∧ closedin X V) ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ W)"
    using assms(1) by(auto simp: locally_compact_space_neighbourhood_base_closedin[OF assms(2)] neighbourhood_base_of)
  from this[OF assms(4)] have "∀x∈T. ∃U W. openin X U ∧ (compactin X W ∧ closedin X W) ∧ x ∈ U ∧ U ⊆ W ∧ W ⊆ V"
    using assms(5) by blast
  then have "∃Ux Wx. ∀x∈T. openin X (Ux x) ∧ compactin X (Wx x) ∧ closedin X (Wx x) ∧ x ∈ Ux x ∧ Ux x ⊆ Wx x ∧ Wx x ⊆ V"
    by metis
  then obtain Ux Wx where UW: "⋀x. x ∈ T ⟹ openin X (Ux x)" "⋀x. x ∈ T ⟹ compactin X (Wx x)" "⋀x. x ∈ T ⟹ closedin X (Wx x)"
   "⋀x. x ∈ T ⟹ x ∈ Ux x" "⋀x. x ∈ T ⟹ Ux x ⊆ Wx x" "⋀x. x ∈ T ⟹ Wx x ⊆ V"
    by blast
  have "T ⊆ (⋃x∈T. Ux x)"
    using UW by blast
  hence "∃ℱ. finite ℱ ∧ ℱ ⊆ Ux ` T ∧ T ⊆ ⋃ ℱ"
    using compactinD[OF assms(3),of "Ux ` T"] UW(1) by auto
  then obtain T' where T': "finite T'" "T' ⊆ T" "T ⊆ (⋃x∈T'. Ux x)"
    by (metis finite_subset_image)
  have 1:"X closure_of ⋃ (Ux ` T') = (⋃x∈T'. X closure_of (Ux x))"
    by (simp add: T'(1) closure_of_Union)
  have 2:"⋀x. x ∈ T' ⟹ X closure_of (Ux x) ⊆ Wx x"
    by (meson T'(2) UW(3) UW(5) closure_of_minimal subsetD)
  hence "⋀x. x ∈ T' ⟹ compactin X (X closure_of (Ux x))"
    by (meson T'(2) UW(2) closed_compactin closedin_closure_of subsetD)
  then show ?thesis
    using T' 2 UW by(fastforce intro!: exI[where x="⋃x∈T'. Ux x"] compactin_Union simp: 1)
qed

lemma Urysohn_locally_compact_Hausdorff_closed_compact_support:
  fixes a b :: real and X :: "'a topology"
  assumes "locally_compact_space X" "Hausdorff_space X ∨ regular_space X"
      and "a ≤ b" "closedin X S" "compactin X T" "disjnt S T"
  obtains f where "continuous_map X (subtopology euclidean {a..b}) f" "f ` S ⊆ {a}" "f ` T ⊆ {b}" "disjnt (X closure_of {x∈topspace X. f x ≠ a}) S" "compactin X (X closure_of {x∈topspace X. f x ≠ a})"
proof -
  have "∃f. continuous_map X (subtopology euclidean {0..1::real}) f ∧ f ` S ⊆ {0} ∧ f ` T ⊆ {1} ∧ disjnt (X closure_of {x∈topspace X. f x ≠ 0}) S ∧  compactin X (X closure_of {x∈topspace X. f x ≠ 0})"
  proof -
    define r :: "nat ⇒ real" where "r ≡ (λn. if n = 0 then 0 else if n = 1 then 1 else from_nat_into ({0<..<1} ∩ ℚ) (n - 2))"
    have r_01: "r 0 = 0" "r (Suc 0) = 1"
      by(simp_all add: r_def)
    have r_bij: "bij_betw r UNIV ({0..1} ∩ ℚ)"
    proof -
      have 1:"bij_betw (from_nat_into ({0<..<1::real} ∩ ℚ)) UNIV ({0<..<1} ∩ ℚ)"
      proof -
        have [simp]:"infinite ({0<..<1::real} ∩ ℚ)"
        proof -
          have "{0<..<1::real} ∩ ℚ = of_rat ` {0<..<1::rat}"
            by(auto simp: Rats_def)
          also have "infinite ..."
          proof
            assume "finite (real_of_rat ` {0<..<1})"
            moreover have "finite (real_of_rat ` {0<..<1}) ⟷ finite {0<..<1::rat}"
              by(auto intro!: finite_image_iff inj_onI)
            ultimately show False
              using infinite_Ioo[of 0 "1 :: rat"] by simp
          qed
          finally show ?thesis .
        qed
        show ?thesis
          using countable_rat by(auto intro!: from_nat_into_to_nat_on_product_metric_pair)
      qed
      have 2: "bij_betw r ({2..}) ({0<..<1} ∩ ℚ)"
      proof -
        have 3:"bij_betw (λn. n - 2) {2::nat..} UNIV"
          by(auto simp: bij_betw_def image_def intro!: inj_onI bexI[where x="_ + 2"])
        have 4:"bij_betw (λn. r (n + 2)) UNIV ({0<..<1} ∩ ℚ)"
          using 1 by(auto simp: r_def)
        have 5:" bij_betw (λn. r (Suc (Suc (n - 2)))) {2..} ({0<..<1} ∩ ℚ)"
          using bij_betw_comp_iff[THEN iffD1,OF 3 4] by(auto simp: comp_def)
        show ?thesis
          by(rule bij_betw_cong[THEN iffD1,OF _ 5]) (simp add: Suc_diff_Suc numeral_2_eq_2) 
      qed
      have [simp]: "insert (Suc 0) (insert 0 {2..}) = UNIV" "insert 1 (insert 0 ({0<..<1::real} ∩ ℚ)) = {0..1} ∩ ℚ"
        by auto
      show ?thesis
        using notIn_Un_bij_betw[of 1,OF _ _ notIn_Un_bij_betw[of 0,OF _ _ 2]] by(auto simp: r_01)
    qed
    have r0_min: "⋀n. n ≠ 0 ⟷ r 0 < r n"
      using r_bij r_01 by (metis (full_types) IntE UNIV_I atLeastAtMost_iff bij_betw_iff_bijections linorder_not_le not_less_iff_gr_or_eq) 
    have r1_max: "⋀n. n ≠ 1 ⟷ r n < r 1"
      using r_bij r_01(2) by (metis (no_types, opaque_lifting) IntD2 One_nat_def UNIV_I atLeastAtMost_iff bij_betw_iff_bijections inf_commute linorder_less_linear linorder_not_le)
    let ?V = "topspace X - S"
    have openinV: "openin X ?V"
      using assms(4) by blast
    have T_sub_V: "T ⊆ ?V"
      by(meson DiffI assms(5,6) compactin_subset_topspace disjnt_iff subset_eq)
    obtain V0 where V0: "openin X V0" "compactin X (X closure_of V0)" "T ⊆ V0" "X closure_of V0 ⊆ ?V"
      using locally_compact_Hausdorff_compactin_openin_subset[OF assms(1,2) assms(5) openinV T_sub_V] by metis
    obtain V1 where V1: "openin X V1" "compactin X (X closure_of V1)" "T ⊆ V1" "X closure_of V1 ⊆ V0"
      using locally_compact_Hausdorff_compactin_openin_subset[OF assms(1,2) assms(5) V0(1,3)] by metis
    text ‹ arg max ›
    have "∃i. i < n ∧ r i < r n ∧ (∀m. m < n ∧ r m < r n ⟶ r m ≤ r i)" if n: "n ≥ 2" for n
    proof -
      have 1:"{m. m < n ∧ r m < r n} ≠ {}"
      proof -
        have "n ≠ 0"
          using n by fastforce
        hence "r n ≠ r 0"
          by (metis UNIV_I r_bij bij_betw_iff_bijections)
        hence "r n > r 0"
          by (metis IntE UNIV_I atLeastAtMost_iff bij_betw_iff_bijections order_less_le r_01(1) r_bij)
        hence "0 ∈ {m. m < n ∧ r n > r m}"
          using n by auto
        thus ?thesis
          by auto
      qed
      have 2:"finite {m. m < n ∧ r n > r m}"
        by auto
      define ri where "ri ≡ Max (r ` {m. m < n ∧ r n > r m})"
      have ri_1: "ri ∈ r ` {m. m < n ∧ r n > r m}"
        unfolding ri_def using 1 2 by auto
      have ri_2: "⋀m. m < n ⟹ r n > r m ⟹ r m ≤ ri"
        unfolding ri_def by(subst Max_ge_iff) (use 1 2 in auto)
      obtain i where i:"ri = r i" "i < n" "r n > r i"
        using ri_1 by auto
      thus ?thesis
        using ri_2 by(auto intro!: exI[where x=i])
    qed
    then obtain i where i: "⋀n. n ≥ 2 ⟹ i n < n" "⋀n. n ≥ 2 ⟹ r (i n) < r n"
                           "⋀n m. n ≥ 2 ⟹ m < n ⟹ r m < r n ⟹ r m ≤ r (i n)"
      by metis
    text ‹ arg min ›
    have "∃j. j < n ∧ r n < r j ∧ (∀m. m < n ∧ r n < r m ⟶ r j ≤ r m)" if n: "n ≥ 2" for n
    proof -
      have 1:"{m. m < n ∧ r n < r m} ≠ {}"
      proof -
        have "n ≠ 1"
          using n by fastforce
        hence "r n ≠ r 1"
          by (metis UNIV_I r_bij bij_betw_iff_bijections)
        hence "r n < r 1"
          by (metis IntE One_nat_def UNIV_I atLeastAtMost_iff bij_betw_iff_bijections order_less_le r_01(2) r_bij)
        hence "1 ∈ {m. m < n ∧ r n < r m}"
          using n by auto
        thus ?thesis
          by auto
      qed
      have 2:"finite {m. m < n ∧ r n < r m}"
        by auto
      define rj where "rj ≡ Min (r ` {m. m < n ∧ r n < r m})"
      have rj_1: "rj ∈ r ` {m. m < n ∧ r n < r m}"
        unfolding rj_def using 1 2 by auto
      have rj_2: "⋀m. m < n ⟹ r n < r m ⟹ rj ≤ r m"
        unfolding rj_def by(subst Min_le_iff) (use 1 2 in auto)
      obtain j where j:"rj = r j" "j < n" "r n < r j"
        using rj_1 by auto
      thus ?thesis
        using rj_2 by(auto intro!: exI[where x=j])
    qed
    then obtain j where j: "⋀n. n ≥ 2 ⟹ j n < n" "⋀n. n ≥ 2 ⟹ r (j n) > r n" "⋀n m. n ≥ 2 ⟹ m < n ⟹ r m > r n ⟹ r m ≥ r (j n)"
      by metis
    have i2: "i 2 = 0" 
      by (metis i(1,2) One_nat_def dual_order.refl less_2_cases not_less_iff_gr_or_eq r1_max)
    have j2: "j 2 = 1"
      by (metis j(1,2) One_nat_def dual_order.refl i(2) i2 less_2_cases not_less_iff_gr_or_eq)
    have "∃Vn. ∀n. Vn n = (if n = 0 then V0 else if n = 1 then V1
       else (SOME V. openin X V ∧ compactin X (X closure_of V) ∧ X closure_of Vn (j n) ⊆ V ∧ X closure_of V ⊆ Vn (i n)))"
      (is "∃Vn. ∀n. Vn n = ?if n Vn")
    proof(rule dependent_wellorder_choice)
      fix r n and Vn Vn' :: "nat ⇒ 'a set"
      assume h:"⋀y::nat. y < n ⟹ Vn y = Vn' y"
      consider "n ≥ 2" | "n = 0" | "n = 1"
        by fastforce
      then show "r = ?if n Vn ⟷ r = ?if n Vn'"
        by cases (use i j h in auto)
    qed auto
    then obtain Vn where Vn_def: "⋀n. Vn n = (if n = 0 then V0 else if n = 1 then V1
       else (SOME V. openin X V ∧ compactin X (X closure_of V) ∧ X closure_of Vn (j n) ⊆ V ∧ X closure_of V ⊆ Vn (i n)))"
      by blast
    have Vn_0: "Vn 0 = V0" and Vn_1: "Vn 1 = V1"
      by(auto simp: Vn_def)
    have Vns: "(n ≥ 2 ⟶ openin X (Vn n) ∧ compactin X (X closure_of Vn n) ∧
                X closure_of Vn (j n) ⊆ Vn n ∧ X closure_of Vn n ⊆ Vn (i n)) ∧
                (∀k≤n. ∀l≤n. r k < r l ⟶ X closure_of Vn l ⊆ Vn k)" (is "?P1 n ∧ ?P2 n") for n
    proof(rule nat_less_induct[of _ n])
      fix n
      assume h:"∀m<n. ?P1 m ∧ ?P2 m"
      show "?P1 n ∧ ?P2 n"
      proof
        show P1:"?P1 n"
        proof
          assume n: "2 ≤ n"
          then consider "n = 2" | "n > 2"
            by fastforce
          then show "openin X (Vn n) ∧ compactin X (X closure_of Vn n) ∧
                     X closure_of Vn (j n) ⊆ Vn n ∧ X closure_of Vn n ⊆ Vn (i n)"
          proof cases
            case 1
            have 2:"Vn 2 = (SOME V. openin X V ∧ compactin X (X closure_of V) ∧
                    X closure_of Vn 1 ⊆ V ∧ X closure_of V ⊆ Vn 0)"
              by(simp add: Vn_def i2 j2 1)
            show ?thesis
              unfolding 1 i2 j2 Vn_0 Vn_1 2
              by(rule someI_ex)
                (auto intro!: V0 V1 locally_compact_Hausdorff_compactin_openin_subset[OF assms(1,2)])
          next
            case 2
            then have 1:"Vn n = (SOME V. openin X V ∧ compactin X (X closure_of V) ∧ X closure_of Vn (j n) ⊆ V ∧ X closure_of V ⊆ Vn (i n))"
              by(auto simp: Vn_def)
            show ?thesis
              unfolding 1
            proof(rule someI_ex)
              have ij:"j n < n" "i n < n" "r (i n) < r (j n)"
                using j[of n] i[of n] order.strict_trans 2 by auto
              hence "max (j n) (i n) < n"
                by auto
              from h[rule_format,OF this] ij(3) have ijsub:"X closure_of Vn (j n) ⊆ Vn (i n)"
                by auto
              have jc:"compactin X (X closure_of Vn (j n))"
              proof -
                consider "j n ≥ 2" | "j n = 0" | "j n = 1"
                  by fastforce
                then show ?thesis
                proof cases
                  case 1
                  then show ?thesis
                    using ij(1) h by auto
                qed(auto simp: Vn_0 Vn_1[simplified] V0 V1)
              qed
              have io:"openin X (Vn (i n))"
              proof -
                consider "i n ≥ 2" | "i n = 0" | "i n = 1"
                  by fastforce
                then show ?thesis
                proof cases
                  case 1
                  then show ?thesis
                    using ij(2) h by auto
                qed(auto simp: Vn_0 Vn_1[simplified] V0 V1)
              qed
              show "∃x. openin X x ∧ compactin X (X closure_of x) ∧ X closure_of Vn (j n) ⊆ x ∧ X closure_of x ⊆ Vn (i n)"
                by(rule locally_compact_Hausdorff_compactin_openin_subset[OF assms(1,2) jc io ijsub])
            qed
          qed
        qed
        show "?P2 n"
        proof(intro allI impI)
          fix k l
          assume kl: "k ≤ n" "l ≤ n" "r k < r l"
          then consider "n = 1" | "n ≥ 2"
            using r_bij order_neq_le_trans by fastforce 
          then show "X closure_of Vn l ⊆ Vn k"
          proof cases
            case 1
            then have [simp]: "k = 0" "l = 1"
              using r_01 kl le_Suc_eq by fastforce+ 
            show ?thesis
              using Vn_0 Vn_1 V0 V1 by simp
          next
            case n:2
            consider "k < n" "l < n" | "k = n" "l < n" | "k < n" "l = n"
              using kl order_less_le by auto
            then show ?thesis
            proof cases
              case 1
              with kl(3) h show ?thesis
                by (meson nle_le)
            next
              case k:2
              then have k1:"X closure_of Vn (j k) ⊆ Vn k"
                using P1 n by simp
              consider "r (j k) = r l" | "r (j k) < r l"
                using j(3)[OF _ _ kl(3)] k n by fastforce
              then show ?thesis
              proof cases
                case 1
                then have "j k = l"
                  using r_bij by(auto simp: bij_betw_def injD)
                with k1 show ?thesis by simp
              next
                case 2
                then have " X closure_of Vn l ⊆ Vn (j k)"
                  using k h by (meson j(1) n nat_le_linear)
                thus ?thesis
                  using k1 closure_of_mono by fastforce
              qed
            next
              case l:3
              consider "r k = r (i l)" | "r k < r (i l)"
                using i(3)[OF _ _ kl(3)] l n by fastforce
              then show ?thesis
              proof cases
                case 1
                then have "k = i l"
                  using r_bij by(auto simp: bij_betw_def injD)
                thus ?thesis
                  using P1 l(2) n by blast 
              next
                case 2
                then have " X closure_of Vn (i l) ⊆ Vn k"
                  by (metis h i(1) l(1) l(2) n nle_le)
                thus ?thesis
                  by (metis P1 closure_of_closure_of closure_of_mono l(2) n subset_trans)
              qed
            qed
          qed
        qed
      qed
    qed

    define Vr where "Vr ≡ (λx. let n = THE n. x = r n in Vn n)"
    have Vr_Vn: "Vr (r n) = Vn n" for n
    proof -
      have 1:"⋀n m. r n = r m ⟷ n = m"
        using r_bij by(auto simp: bij_betw_def injD)
      have [simp]:"(THE m. r n = r m) = n"
        by(auto simp: 1)
      show ?thesis
        by(simp add: Vr_def)
    qed
    have Vr0: "Vr 0 = V0"
      using Vr_Vn[of 0] by(auto simp: Vn_0 r_01)
    have Vr1: "Vr 1 = V1"
      using Vr_Vn[of 1] Vn_1 by(auto simp: r_01)
    have openin_Vr: "openin X (Vr s)" if s:"s ∈ {0..1} ∩ ℚ" for s
    proof -
      consider "0 < s" "s < 1" | "s = 0" | "s = 1"
        using s by fastforce
      then show ?thesis
      proof cases
        case 1
        then obtain n where "n ≥ 2" "s = r n"
          by (metis r0_min r1_max s One_nat_def Suc_1 bij_betw_iff_bijections bot_nat_0.extremum_unique le_SucE not_less_eq_eq r_bij r_def)
        thus ?thesis
          using Vns Vr_Vn by fastforce
      qed(auto simp: Vr0 Vr1 V0 V1)
    qed
    have compactin_clVr: "compactin X (X closure_of (Vr s))" if s:"s ∈ {0..1} ∩ ℚ" for s
    proof -
      consider "0 < s" "s < 1" | "s = 0" | "s = 1"
        using s by fastforce
      then show ?thesis
      proof cases
        case 1
        then obtain n where "n ≥ 2" "s = r n"
          by (metis r0_min r1_max s One_nat_def Suc_1 bij_betw_iff_bijections bot_nat_0.extremum_unique le_SucE not_less_eq_eq r_bij r_def)
        thus ?thesis
          using Vns Vr_Vn by fastforce
      qed(auto simp: Vr0 Vr1 V0 V1)
    qed
    have Vr_antimono:"X closure_of Vr s ⊆ Vr k" if h:"s ∈ {0..1} ∩ ℚ" "k ∈ {0..1} ∩ ℚ" "k < s" for k s
    proof -
      obtain ns nk where n: "s = r ns" "k = r nk"
        by (metis h(1,2) bij_betw_iff_bijections r_bij)
      show ?thesis
        using Vr_Vn Vns[of "max ns nk"] h by(auto simp: n)
    qed
    define f where "f ≡ (λx. ⨆s∈{0..1} ∩ ℚ. s * indicat_real (Vr s) x)" 
    define g where "g ≡ (λx. ⨅s∈{0..1} ∩ ℚ. (1 - s) * indicat_real (X closure_of Vr s) x + s)"
    note [intro!] = bdd_belowI[where m=0] bdd_aboveI[where M=1]
    note [simp] = mult_le_one
    have ne[simp]: "{0..1::real} ∩ ℚ ≠ {}"
      using Rats_0 atLeastAtMost_iff zero_less_one_class.zero_le_one by blast
      
    have f_lower:"lower_semicontinuous_map X f"
      unfolding f_def
      by(auto intro!: lower_semicontinuous_map_cSup lower_semicontinuous_map_real_cmult indicator_open_lower_semicontinuous_map openin_Vr)
    have g_upper:"upper_semicontinuous_map X g"
      unfolding g_def
      by(auto intro!: upper_semicontinuous_map_cInf upper_semicontinuous_map_real_cmult indicator_closed_upper_semicontinuous_map
                simp: upper_semicontinuous_map_add_c_iff)

    have f_01: "⋀x. 0 ≤ f x" "⋀x. f x ≤ 1"
    proof -
      show "⋀x. 0 ≤ f x"
        unfolding f_def by(subst le_cSup_iff) (auto intro!: bexI[where x=0])
      show "⋀x. f x ≤ 1"
        unfolding f_def by(subst cSup_le_iff) (auto intro!: bexI[where x=0])
    qed
    have g_01: "⋀x. 0 ≤ g x" "⋀x. g x ≤ 1"
    proof -
      show "⋀x. 0 ≤ g x"
        unfolding g_def by(subst le_cInf_iff) auto
      have "⋀x. ∀y>1. ∃a∈(λs. (1 - s) * indicat_real (X closure_of Vr s) x + s) ` ({0..1} ∩ ℚ). a < y"
        by (metis (no_types, lifting) Int_iff Rats_1 add_0 atLeastAtMost_iff cancel_comm_monoid_add_class.diff_cancel image_eqI less_eq_real_def mult_cancel_left1 zero_less_one_class.zero_le_one)
      thus "⋀x. g x ≤ 1"
        unfolding g_def by(subst cInf_le_iff) auto
    qed

    have disj: "disjnt (X closure_of {x∈topspace X. f x ≠ 0}) S"
      and f_csupport:"compactin X (X closure_of {x∈topspace X. f x ≠ 0})"
    proof -
      have 1:"{x∈topspace X. f x ≠ 0} ⊆ X closure_of V0"
      proof -
        have "{x∈topspace X. f x ≠ 0} = {x∈topspace X. f x > 0}"
          using f_01 by (simp add: order_less_le)
        also have "... ⊆ X closure_of V0"
        proof safe
          fix x
          assume h:"x ∈ topspace X" "0 < f x"
          then have "∃x∈(λs. s * indicat_real (Vr s) x) ` ({0..1} ∩ ℚ). 0 < x"
            by(intro less_cSup_iff[THEN iffD1]) (auto simp: f_def)
          then obtain s where s: "s ∈ {0..1} ∩ ℚ" "s * indicat_real (Vr s) x > 0"
            by fastforce
          hence 1:"s > 0" "0 < indicat_real (Vr s) x"
            by (auto simp add: zero_less_mult_iff)
          hence 2:"x ∈ Vr s"
            by(auto simp: indicator_def)
          have "Vr s ⊆ X closure_of Vr s"
            by (meson closure_of_subset openin_Vr openin_subset s(1))
          also have "... ⊆ X closure_of V0"
            using Vr_antimono[OF _ _ 1(1)] s(1) by (metis IntI Rats_0 Vr0 atLeastAtMost_iff calculation closure_of_mono order.refl order_trans zero_less_one_class.zero_le_one)
          finally show "x ∈ X closure_of V0"
            using 2 by auto
        qed
        finally show ?thesis .
      qed
      thus "compactin X (X closure_of {x∈topspace X. f x ≠ 0})"
        by (meson V0(2) closed_compactin closedin_closure_of closure_of_minimal)
      show "disjnt (X closure_of {x∈topspace X. f x ≠ 0}) S"
        using 1 V0(4) closure_of_mono by(fastforce simp: disjnt_def)
    qed
    have f_1: "f x = 1" if x: "x ∈ T" for x
    proof -
      have xv:"x ∈ V1"
        using V1(3) x by blast
      have "1 ≤ f x"
        unfolding f_def by(subst le_cSup_iff) (auto intro!: bexI[where x=1] simp: Vr1 xv)
      with f_01 show ?thesis
        using nle_le by blast
    qed
    have f_0: "f x = 0" if x: "x ∈ S" for x
    proof -
      have "x ∉ Vr s" if s: "s ∈ {0..1} ∩ ℚ"for s
      proof -
        have "x ∉ Vr 0"
          using x V0 closure_of_subset[OF openin_subset[of X V0]] by(auto simp: Vr0)
        moreover have "Vr s ⊆ Vr 0"
          using Vr_antimono[of s 0] s closure_of_subset[OF openin_subset[OF openin_Vr[OF s]]]
          by(cases "s = 0") auto
        ultimately show ?thesis
          by blast
      qed
      hence "f x ≤ 0"
        unfolding f_def by(subst cSup_le_iff) auto
      with f_01 show ?thesis
        using nle_le by blast
    qed
    have fg:"f x = g x" if x: "x ∈ topspace X" for x
    proof -
      have "¬ f x < g x"
      proof
        assume "f x < g x"
        then obtain r s where rs: "r ∈ ℚ" "s ∈ ℚ" "f x < r" "r < s" "s < g x"
          by (meson Rats_dense_in_real)
        hence r:"r ∈ {0..1} ∩ ℚ"
          using f_01 g_01 by (metis IntI atLeastAtMost_iff inf.orderE inf.strict_coboundedI2 linorder_not_less nle_le)
        hence s:"s ∈ {0..1} ∩ ℚ"
          using g_01 rs by (metis IntI atLeastAtMost_iff f_01(1) inf.strict_coboundedI2 inf.strict_order_iff less_eq_real_def)
        have x1:"x ∉ Vr r"
        proof -
          have "r * indicat_real (Vr r) x < r"
            using r by(auto intro!: cSUP_lessD[OF _ rs(3)[simplified f_def]])
          thus ?thesis
            using r by auto
        qed
        have x2:"x ∈ X closure_of Vr s"
        proof -
          have 1:"s < (1 - s) * indicat_real (X closure_of Vr s) x + s"
            using s by(intro less_cINF_D[OF _ rs(5)[simplified g_def]]) auto
          show ?thesis
            by(rule ccontr) (use s 1 in auto)
        qed
        show False
          using x1 x2 Vr_antimono[OF s r rs(4)] by blast
      qed
      moreover have "f x ≤ g x"
      proof -
        have "l * indicat_real (Vr l) x ≤ (1 - s) * indicat_real (X closure_of Vr s) x + s"
          if ls: "l ∈ {0..1} ∩ ℚ" "s ∈ {0..1} ∩ ℚ" for l s
        proof(rule ccontr)
          assume h:"¬ l * indicat_real (Vr l) x ≤ (1 - s) * indicat_real (X closure_of Vr s) x + s"
          then have "l * indicat_real (Vr l) x > (1 - s) * indicat_real (X closure_of Vr s) x + s"
            by auto
          hence "l > s ∧ x ∈ Vr l ∧ x ∉ Vr s"
            using ls by (metis (no_types, opaque_lifting) h Int_iff add.commute add.right_neutral atLeastAtMost_iff closure_of_subset diff_add_cancel in_mono indicator_simps(1) indicator_simps(2) mult.commute mult_1 mult_zero_left openin_Vr openin_subset zero_less_one_class.zero_le_one)
          moreover have "Vr l ⊆ Vr s"
            using Vr_antimono[OF ls] by (meson calculation closure_of_subset ls(1) openin_Vr openin_subset order_trans)
          ultimately show False
            by blast
        qed
        thus "f x ≤ g x"
          unfolding f_def g_def by(auto intro!: cSup_le_iff[THEN iffD2] le_cInf_iff[THEN iffD2])
      qed
      ultimately show ?thesis
        by simp
    qed
    show ?thesis
    proof(safe intro!: exI[where x=f])
      have "continuous_map X euclideanreal f"
        by (simp add: fg f_lower g_upper upper_lower_semicontinuous_map_iff_continuous_map upper_semicontinuous_map_cong)
      thus "continuous_map X (top_of_set {0..1}) f"
        using f_01 by(auto simp: continuous_map_in_subtopology)
    qed(use f_0 f_1 f_csupport disj in auto)
  qed
  then obtain f where f: "continuous_map X (top_of_set {0..1}) f" "f ` S ⊆ {0::real}" "f ` T ⊆ {1}"
    "disjnt (X closure_of {x∈topspace X. f x ≠ 0}) S" "compactin X (X closure_of {x ∈ topspace X. f x ≠ 0})"
    by blast
  define g where "g ≡ (λx. (b - a) * f x + a)"
  have "continuous_map X (top_of_set {a..b}) g"
  proof -
    have [simp]:"0 ≤ y ∧ y ≤ 1 ⟹ (b - a) * y + a ≤ b" for y
      using assms(3) by (meson diff_ge_0_iff_ge le_diff_eq mult_left_le)
    show ?thesis
      unfolding continuous_map_in_subtopology
    proof (rule conjI)
      show "continuous_map X euclideanreal g"
        using f(1)
        by (auto simp: continuous_map_in_subtopology g_def
            intro: continuous_map_add continuous_map_real_mult_left)
    next
      show "g ∈ topspace X → {a..b}"
        using f(1) assms(3)
        by (auto simp add: continuous_map_in_subtopology g_def Pi_iff
            simp flip: image_subset_iff_funcset)
    qed
  qed  
  moreover have "g ` S ⊆ {a}" "g ` T ⊆ {b}"
    using f(2,3) by(auto simp: g_def)
  moreover have "disjnt (X closure_of {x∈topspace X. g x ≠ a}) S"
                "compactin X (X closure_of {x ∈ topspace X. g x ≠ a})"
  proof -
    consider "a = b" | "a < b"
      using assms by fastforce
    then have "disjnt (X closure_of {x∈topspace X. g x ≠ a}) S ∧ compactin X (X closure_of {x ∈ topspace X. g x ≠ a})"
    proof cases
      case 1
      then have [simp]:"{x ∈ topspace X. g x ≠ a} = {}"
        by(auto simp: g_def)
      thus ?thesis
        by simp_all
    next
      case 2
      then have "{x ∈ topspace X. g x ≠ a} = {x ∈ topspace X. f x ≠ 0}"
        by(auto simp: g_def)
      thus ?thesis
        by(simp add: f)
    qed
    thus "disjnt (X closure_of {x∈topspace X. g x ≠ a}) S" "compactin X (X closure_of {x ∈ topspace X. g x ≠ a})"
      by simp_all
  qed
  ultimately show ?thesis
    using that by auto
qed

end