# Theory Further_Topology

```section ‹Extending Continous Maps, Invariance of Domain, etc› (*FIX rename? *)

text‹Ported from HOL Light (moretop.ml) by L C Paulson›

theory Further_Topology
imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts
begin

subsection‹A map from a sphere to a higher dimensional sphere is nullhomotopic›

lemma spheremap_lemma1:
fixes f :: "'a::euclidean_space ⇒ 'a::euclidean_space"
assumes "subspace S" "subspace T" and dimST: "dim S < dim T"
and "S ⊆ T"
and diff_f: "f differentiable_on sphere 0 1 ∩ S"
shows "f ` (sphere 0 1 ∩ S) ≠ sphere 0 1 ∩ T"
proof
assume fim: "f ` (sphere 0 1 ∩ S) = sphere 0 1 ∩ T"
have inS: "⋀x. ⟦x ∈ S; x ≠ 0⟧ ⟹ (x /⇩R norm x) ∈ S"
using subspace_mul ‹subspace S› by blast
have subS01: "(λx. x /⇩R norm x) ` (S - {0}) ⊆ sphere 0 1 ∩ S"
using ‹subspace S› subspace_mul by fastforce
then have diff_f': "f differentiable_on (λx. x /⇩R norm x) ` (S - {0})"
by (rule differentiable_on_subset [OF diff_f])
define g where "g ≡ λx. norm x *⇩R f(inverse(norm x) *⇩R x)"
have gdiff: "g differentiable_on S - {0}"
unfolding g_def
by (rule diff_f' derivative_intros differentiable_on_compose [where f=f] | force)+
have geq: "g ` (S - {0}) = T - {0}"
proof
have "⋀u. ⟦u ∈ S; norm u *⇩R f (u /⇩R norm u) ∉ T⟧ ⟹ u = 0"
by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF ‹subspace T›] fim image_subset_iff inf_le2 singletonD)
then have "g ` (S - {0}) ⊆ T"
using g_def by blast
moreover have "g ` (S - {0}) ⊆ UNIV - {0}"
proof (clarsimp simp: g_def)
fix y
assume "y ∈ S" and f0: "f (y /⇩R norm y) = 0"
then have "y ≠ 0 ⟹ y /⇩R norm y ∈ sphere 0 1 ∩ S"
by (auto simp: subspace_mul [OF ‹subspace S›])
then show "y = 0"
by (metis fim f0 Int_iff image_iff mem_sphere_0 norm_eq_zero zero_neq_one)
qed
ultimately show "g ` (S - {0}) ⊆ T - {0}"
by auto
next
have *: "sphere 0 1 ∩ T ⊆ f ` (sphere 0 1 ∩ S)"
using fim by (simp add: image_subset_iff)
have "x ∈ (λx. norm x *⇩R f (x /⇩R norm x)) ` (S - {0})"
if "x ∈ T" "x ≠ 0" for x
proof -
have "x /⇩R norm x ∈ T"
using ‹subspace T› subspace_mul that by blast
then obtain u where u: "f u ∈ T" "x /⇩R norm x = f u" "norm u = 1" "u ∈ S"
using * [THEN subsetD, of "x /⇩R norm x"] ‹x ≠ 0› by auto
with that have [simp]: "norm x *⇩R f u = x"
by (metis divideR_right norm_eq_zero)
moreover have "norm x *⇩R u ∈ S - {0}"
using ‹subspace S› subspace_scale that(2) u by auto
with u show ?thesis
by (simp add: image_eqI [where x="norm x *⇩R u"])
qed
then have "T - {0} ⊆ (λx. norm x *⇩R f (x /⇩R norm x)) ` (S - {0})"
by force
then show "T - {0} ⊆ g ` (S - {0})"
qed
define T' where "T' ≡ {y. ∀x ∈ T. orthogonal x y}"
have "subspace T'"
have dim_eq: "dim T' + dim T = DIM('a)"
using dim_subspace_orthogonal_to_vectors [of T UNIV] ‹subspace T›
have "∃v1 v2. v1 ∈ span T ∧ (∀w ∈ span T. orthogonal v2 w) ∧ x = v1 + v2" for x
by (force intro: orthogonal_subspace_decomp_exists [of T x])
then obtain p1 p2 where p1span: "p1 x ∈ span T"
and "⋀w. w ∈ span T ⟹ orthogonal (p2 x) w"
and eq: "p1 x + p2 x = x" for x
by metis
then have p1: "⋀z. p1 z ∈ T" and ortho: "⋀w. w ∈ T ⟹ orthogonal (p2 x) w" for x
using span_eq_iff ‹subspace T› by blast+
then have p2: "⋀z. p2 z ∈ T'"
have p12_eq: "⋀x y. ⟦x ∈ T; y ∈ T'⟧ ⟹ p1(x + y) = x ∧ p2(x + y) = y"
proof (rule orthogonal_subspace_decomp_unique [OF eq p1span, where T=T'])
show "⋀x y. ⟦x ∈ T; y ∈ T'⟧ ⟹ p2 (x + y) ∈ span T'"
using span_eq_iff p2 ‹subspace T'› by blast
show "⋀a b. ⟦a ∈ T; b ∈ T'⟧ ⟹ orthogonal a b"
using T'_def by blast
qed (auto simp: span_base)
then have "⋀c x. p1 (c *⇩R x) = c *⇩R p1 x ∧ p2 (c *⇩R x) = c *⇩R p2 x"
proof -
fix c :: real and x :: 'a
have f1: "c *⇩R x = c *⇩R p1 x + c *⇩R p2 x"
by (metis eq pth_6)
have f2: "c *⇩R p2 x ∈ T'"
by (simp add: ‹subspace T'› p2 subspace_scale)
have "c *⇩R p1 x ∈ T"
by (metis (full_types) assms(2) p1span span_eq_iff subspace_scale)
then show "p1 (c *⇩R x) = c *⇩R p1 x ∧ p2 (c *⇩R x) = c *⇩R p2 x"
using f2 f1 p12_eq by presburger
qed
moreover have lin_add: "⋀x y. p1 (x + y) = p1 x + p1 y ∧ p2 (x + y) = p2 x + p2 y"
proof (rule orthogonal_subspace_decomp_unique [OF _ p1span, where T=T'])
show "⋀x y. p1 (x + y) + p2 (x + y) = p1 x + p1 y + (p2 x + p2 y)"
show  "⋀a b. ⟦a ∈ T; b ∈ T'⟧ ⟹ orthogonal a b"
using T'_def by blast
qed (auto simp: p1span p2 span_base span_add)
ultimately have "linear p1" "linear p2"
by unfold_locales auto
have "g differentiable_on p1 ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}"
using p12_eq ‹S ⊆ T›  by (force intro: differentiable_on_subset [OF gdiff])
then have "(λz. g (p1 z)) differentiable_on {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}"
by (rule differentiable_on_compose [OF linear_imp_differentiable_on [OF ‹linear p1›]])
then have diff: "(λx. g (p1 x) + p2 x) differentiable_on {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}"
by (intro derivative_intros linear_imp_differentiable_on [OF ‹linear p2›])
have "dim {x + y |x y. x ∈ S - {0} ∧ y ∈ T'} ≤ dim {x + y |x y. x ∈ S  ∧ y ∈ T'}"
by (blast intro: dim_subset)
also have "... = dim S + dim T' - dim (S ∩ T')"
using dim_sums_Int [OF ‹subspace S› ‹subspace T'›]
also have "... < DIM('a)"
using dimST dim_eq by auto
finally have neg: "negligible {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}"
by (rule negligible_lowdim)
have "negligible ((λx. g (p1 x) + p2 x) ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'})"
by (rule negligible_differentiable_image_negligible [OF order_refl neg diff])
then have "negligible {x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'}"
proof (rule negligible_subset)
have "⟦t' ∈ T'; s ∈ S; s ≠ 0⟧
⟹ g s + t' ∈ (λx. g (p1 x) + p2 x) `
{x + t' |x t'. x ∈ S ∧ x ≠ 0 ∧ t' ∈ T'}" for t' s
using ‹S ⊆ T› p12_eq  by (rule_tac x="s + t'" in image_eqI) auto
then show "{x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'}
⊆ (λx. g (p1 x) + p2 x) ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}"
by auto
qed
moreover have "- T' ⊆ {x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'}"
proof clarsimp
fix z assume "z ∉ T'"
show "∃x y. z = x + y ∧ x ∈ g ` (S - {0}) ∧ y ∈ T'"
by (metis Diff_iff ‹z ∉ T'› add.left_neutral eq geq p1 p2 singletonD)
qed
ultimately have "negligible (-T')"
using negligible_subset by blast
moreover have "negligible T'"
using negligible_lowdim
ultimately have  "negligible (-T' ∪ T')"
by (metis negligible_Un_eq)
then show False
using negligible_Un_eq non_negligible_UNIV by simp
qed

lemma spheremap_lemma2:
fixes f :: "'a::euclidean_space ⇒ 'a::euclidean_space"
assumes ST: "subspace S" "subspace T" "dim S < dim T"
and "S ⊆ T"
and contf: "continuous_on (sphere 0 1 ∩ S) f"
and fim: "f ` (sphere 0 1 ∩ S) ⊆ sphere 0 1 ∩ T"
shows "∃c. homotopic_with_canon (λx. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) f (λx. c)"
proof -
have [simp]: "⋀x. ⟦norm x = 1; x ∈ S⟧ ⟹ norm (f x) = 1"
using fim by (simp add: image_subset_iff)
have "compact (sphere 0 1 ∩ S)"
by (simp add: ‹subspace S› closed_subspace compact_Int_closed)
then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 ∩ S) ⊆ T"
and g12: "⋀x. x ∈ sphere 0 1 ∩ S ⟹ norm(f x - g x) < 1/2"
using Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ ‹subspace T›, of "1/2"] fim by auto
have gnz: "g x ≠ 0" if "x ∈ sphere 0 1 ∩ S" for x
proof -
have "norm (f x) = 1"
using fim that by (simp add: image_subset_iff)
then show ?thesis
using g12 [OF that] by auto
qed
have diffg: "g differentiable_on sphere 0 1 ∩ S"
by (metis pfg differentiable_on_polynomial_function)
define h where "h ≡ λx. inverse(norm(g x)) *⇩R g x"
have h: "x ∈ sphere 0 1 ∩ S ⟹ h x ∈ sphere 0 1 ∩ T" for x
unfolding h_def
using gnz [of x]
by (auto simp: subspace_mul [OF ‹subspace T›] subsetD [OF gim])
have diffh: "h differentiable_on sphere 0 1 ∩ S"
unfolding h_def using gnz
by (fastforce intro: derivative_intros diffg differentiable_on_compose [OF diffg])
have homfg: "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (T - {0}) f g"
proof (rule homotopic_with_linear [OF contf])
show "continuous_on (sphere 0 1 ∩ S) g"
using pfg by (simp add: differentiable_imp_continuous_on diffg)
next
have non0fg: "0 ∉ closed_segment (f x) (g x)" if "norm x = 1" "x ∈ S" for x
proof -
have "f x ∈ sphere 0 1"
using fim that by (simp add: image_subset_iff)
moreover have "norm(f x - g x) < 1/2"
using g12 that by auto
ultimately show ?thesis
by (auto simp: norm_minus_commute dest: segment_bound)
qed
show "closed_segment (f x) (g x) ⊆ T - {0}" if "x ∈ sphere 0 1 ∩ S" for x
proof -
have "convex T"
by (simp add: ‹subspace T› subspace_imp_convex)
then have "convex hull {f x, g x} ⊆ T"
by (metis IntD2 closed_segment_subset fim gim image_subset_iff segment_convex_hull that)
then show ?thesis
using that non0fg segment_convex_hull by fastforce
qed
qed
obtain d where d: "d ∈ (sphere 0 1 ∩ T) - h ` (sphere 0 1 ∩ S)"
using h spheremap_lemma1 [OF ST ‹S ⊆ T› diffh] by force
then have non0hd: "0 ∉ closed_segment (h x) (- d)" if "norm x = 1" "x ∈ S" for x
using midpoint_between [of 0 "h x" "-d"] that h [of x]
by (auto simp: between_mem_segment midpoint_def)
have conth: "continuous_on (sphere 0 1 ∩ S) h"
using differentiable_imp_continuous_on diffh by blast
have hom_hd: "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (T - {0}) h (λx. -d)"
proof (rule homotopic_with_linear [OF conth continuous_on_const])
fix x
assume x: "x ∈ sphere 0 1 ∩ S"
have "convex hull {h x, - d} ⊆ T"
proof (rule hull_minimal)
show "{h x, - d} ⊆ T"
using h d x by (force simp: subspace_neg [OF ‹subspace T›])
qed (simp add: subspace_imp_convex [OF ‹subspace T›])
with x segment_convex_hull show "closed_segment (h x) (- d) ⊆ T - {0}"
by (auto simp add: subset_Diff_insert non0hd)
qed
have conT0: "continuous_on (T - {0}) (λy. inverse(norm y) *⇩R y)"
by (intro continuous_intros) auto
have sub0T: "(λy. y /⇩R norm y) ∈ (T - {0}) → sphere 0 1 ∩ T"
by (fastforce simp: assms(2) subspace_mul)
obtain c where homhc: "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) h (λx. c)"
proof
show "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) h (λx. - d)"
using d
by (force simp: h_def
intro: homotopic_with_eq homotopic_with_compose_continuous_left [OF hom_hd conT0 sub0T])
qed
have "homotopic_with_canon (λx. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) f h"
by (force simp: h_def
intro:  homotopic_with_eq homotopic_with_compose_continuous_left [OF homfg conT0 sub0T])
then show ?thesis
by (metis homotopic_with_trans [OF _ homhc])
qed

lemma spheremap_lemma3:
assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S ≤ dim U"
obtains T where "subspace T" "T ⊆ U" "S ≠ {} ⟹ aff_dim T = aff_dim S"
"(rel_frontier S) homeomorphic (sphere 0 1 ∩ T)"
proof (cases "S = {}")
case True
with ‹subspace U› subspace_0 show ?thesis
by (rule_tac T = "{0}" in that) auto
next
case False
then obtain a where "a ∈ S"
by auto
then have affS: "aff_dim S = int (dim ((λx. -a+x) ` S))"
by (metis hull_inc aff_dim_eq_dim)
with affSU have "dim ((λx. -a+x) ` S) ≤ dim U"
by linarith
with choose_subspace_of_subspace
obtain T where "subspace T" "T ⊆ span U" and dimT: "dim T = dim ((λx. -a+x) ` S)" .
show ?thesis
proof (rule that [OF ‹subspace T›])
show "T ⊆ U"
using span_eq_iff ‹subspace U› ‹T ⊆ span U› by blast
show "aff_dim T = aff_dim S"
using dimT ‹subspace T› affS aff_dim_subspace by fastforce
show "rel_frontier S homeomorphic sphere 0 1 ∩ T"
proof -
have "aff_dim (ball 0 1 ∩ T) = aff_dim (T)"
by (metis IntI interior_ball ‹subspace T› aff_dim_convex_Int_nonempty_interior centre_in_ball empty_iff inf_commute subspace_0 subspace_imp_convex zero_less_one)
then have affS_eq: "aff_dim S = aff_dim (ball 0 1 ∩ T)"
using ‹aff_dim T = aff_dim S› by simp
have "rel_frontier S homeomorphic rel_frontier(ball 0 1 ∩ T)"
proof (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF ‹convex S› ‹bounded S›])
show "convex (ball 0 1 ∩ T)"
by (simp add: ‹subspace T› convex_Int subspace_imp_convex)
show "bounded (ball 0 1 ∩ T)"
show "aff_dim S = aff_dim (ball 0 1 ∩ T)"
by (rule affS_eq)
qed
also have "... = frontier (ball 0 1) ∩ T"
proof (rule convex_affine_rel_frontier_Int [OF convex_ball])
show "affine T"
by (simp add: ‹subspace T› subspace_imp_affine)
show "interior (ball 0 1) ∩ T ≠ {}"
using ‹subspace T› subspace_0 by force
qed
also have "... = sphere 0 1 ∩ T"
by auto
finally show ?thesis .
qed
qed
qed

proposition inessential_spheremap_lowdim_gen:
fixes f :: "'M::euclidean_space ⇒ 'a::euclidean_space"
assumes "convex S" "bounded S" "convex T" "bounded T"
and affST: "aff_dim S < aff_dim T"
and contf: "continuous_on (rel_frontier S) f"
and fim: "f ∈ (rel_frontier S) → rel_frontier T"
obtains c where "homotopic_with_canon (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)"
proof (cases "S = {}")
case True
then show ?thesis
using homotopic_with_canon_on_empty that by auto
next
case False
then show ?thesis
proof (cases "T = {}")
case True
then have "rel_frontier S = {}" "rel_frontier T = {}"
using fim by fastforce+
then show ?thesis
using that by (simp add: homotopic_on_emptyI)
next
case False
obtain T':: "'a set"
where "subspace T'" and affT': "aff_dim T' = aff_dim T"
and homT: "rel_frontier T homeomorphic sphere 0 1 ∩ T'"
using ‹T ≠ {}›  spheremap_lemma3 [OF ‹bounded T› ‹convex T› subspace_UNIV, where 'b='a]
with homeomorphic_imp_homotopy_eqv
have relT: "sphere 0 1 ∩ T'  homotopy_eqv rel_frontier T"
using homotopy_equivalent_space_sym by blast
have "aff_dim S ≤ int (dim T')"
using affT' ‹subspace T'› affST aff_dim_subspace by force
with spheremap_lemma3 [OF ‹bounded S› ‹convex S› ‹subspace T'›] ‹S ≠ {}›
obtain S':: "'a set" where "subspace S'" "S' ⊆ T'"
and affS': "aff_dim S' = aff_dim S"
and homT: "rel_frontier S homeomorphic sphere 0 1 ∩ S'"
by metis
with homeomorphic_imp_homotopy_eqv
have relS: "sphere 0 1 ∩ S'  homotopy_eqv rel_frontier S"
using homotopy_equivalent_space_sym by blast
have dimST': "dim S' < dim T'"
by (metis ‹S' ⊆ T'› ‹subspace S'› ‹subspace T'› affS' affST affT' less_irrefl not_le subspace_dim_equal)
have "∃c. homotopic_with_canon (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)"
using spheremap_lemma2 homotopy_eqv_cohomotopic_triviality_null[OF relS]
using homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim]
by (metis ‹S' ⊆ T'› ‹subspace S'› ‹subspace T'› dimST' image_subset_iff_funcset)
with that show ?thesis by blast
qed
qed

lemma inessential_spheremap_lowdim:
fixes f :: "'M::euclidean_space ⇒ 'a::euclidean_space"
assumes
"DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ∈ (sphere a r) → (sphere b s)"
obtains c where "homotopic_with_canon (λz. True) (sphere a r) (sphere b s) f (λx. c)"
proof (cases "s ≤ 0")
case True then show ?thesis
by (meson nullhomotopic_into_contractible f contractible_sphere that)
next
case False
show ?thesis
proof (cases "r ≤ 0")
case True then show ?thesis
by (meson f nullhomotopic_from_contractible contractible_sphere that)
next
case False
with ‹¬ s ≤ 0› have "r > 0" "s > 0" by auto
show thesis
using inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f]
using ‹0 < r› ‹0 < s› assms(1) that by (auto simp add: f aff_dim_cball)
qed
qed

subsection‹ Some technical lemmas about extending maps from cell complexes›

lemma extending_maps_Union_aux:
assumes fin: "finite ℱ"
and "⋀S. S ∈ ℱ ⟹ closed S"
and "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ; S ≠ T⟧ ⟹ S ∩ T ⊆ K"
and "⋀S. S ∈ ℱ ⟹ ∃g. continuous_on S g ∧ g ` S ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)"
shows "∃g. continuous_on (⋃ℱ) g ∧ g ` (⋃ℱ) ⊆ T ∧ (∀x ∈ ⋃ℱ ∩ K. g x = h x)"
using assms
proof (induction ℱ)
case empty show ?case by simp
next
case (insert S ℱ)
then obtain f where contf: "continuous_on (S) f" and fim: "f ` S ⊆ T" and feq: "∀x ∈ S ∩ K. f x = h x"
by (meson insertI1)
obtain g where contg: "continuous_on (⋃ℱ) g" and gim: "g ` ⋃ℱ ⊆ T" and geq: "∀x ∈ ⋃ℱ ∩ K. g x = h x"
using insert by auto
have fg: "f x = g x" if "x ∈ T" "T ∈ ℱ" "x ∈ S" for x T
proof -
have "T ∩ S ⊆ K ∨ S = T"
using that by (metis (no_types) insert.prems(2) insertCI)
then show ?thesis
using UnionI feq geq ‹S ∉ ℱ› subsetD that by fastforce
qed
moreover have "continuous_on (S ∪ ⋃ ℱ) (λx. if x ∈ S then f x else g x)"
by (auto simp: insert closed_Union contf contg  intro: fg continuous_on_cases)
ultimately show ?case
by (smt (verit, del_insts) Int_iff UnE complete_lattice_class.Sup_insert feq fim geq gim image_subset_iff)
qed

lemma extending_maps_Union:
assumes fin: "finite ℱ"
and "⋀S. S ∈ ℱ ⟹ ∃g. continuous_on S g ∧ g ` S ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)"
and "⋀S. S ∈ ℱ ⟹ closed S"
and K: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ; ¬ X ⊆ Y; ¬ Y ⊆ X⟧ ⟹ X ∩ Y ⊆ K"
shows "∃g. continuous_on (⋃ℱ) g ∧ g ` (⋃ℱ) ⊆ T ∧ (∀x ∈ ⋃ℱ ∩ K. g x = h x)"
apply (simp flip: Union_maximal_sets [OF fin])
apply (rule extending_maps_Union_aux)
apply (simp_all add: Union_maximal_sets [OF fin] assms)
by (metis K psubsetI)

lemma extend_map_lemma:
assumes "finite ℱ" "𝒢 ⊆ ℱ" "convex T" "bounded T"
and poly: "⋀X. X ∈ ℱ ⟹ polytope X"
and aff: "⋀X. X ∈ ℱ - 𝒢 ⟹ aff_dim X < aff_dim T"
and face: "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ⟧ ⟹ (S ∩ T) face_of S"
and contf: "continuous_on (⋃𝒢) f" and fim: "f ` (⋃𝒢) ⊆ rel_frontier T"
obtains g where "continuous_on (⋃ℱ) g" "g ` (⋃ℱ) ⊆ rel_frontier T" "⋀x. x ∈ ⋃𝒢 ⟹ g x = f x"
proof (cases "ℱ - 𝒢 = {}")
case True
show ?thesis
proof
show "continuous_on (⋃ ℱ) f"
using True ‹𝒢 ⊆ ℱ› contf by auto
show "f ` ⋃ ℱ ⊆ rel_frontier T"
using True fim by auto
qed auto
next
case False
then have "0 ≤ aff_dim T"
by (metis aff aff_dim_empty aff_dim_geq aff_dim_negative_iff all_not_in_conv not_less)
then obtain i::nat where i: "int i = aff_dim T"
by (metis nonneg_eq_int)
have Union_empty_eq: "⋃{D. D = {} ∧ P D} = {}" for P :: "'a set ⇒ bool"
by auto
have face': "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ⟧ ⟹ (S ∩ T) face_of S ∧ (S ∩ T) face_of T"
by (metis face inf_commute)
have extendf: "∃g. continuous_on (⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < i})) g ∧
g ` (⋃ (𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < i})) ⊆ rel_frontier T ∧
(∀x ∈ ⋃𝒢. g x = f x)"
if "i ≤ aff_dim T" for i::nat
using that
proof (induction i)
case 0
show ?case
using 0 contf fim by (auto simp add: Union_empty_eq)
next
case (Suc p)
with ‹bounded T› have "rel_frontier T ≠ {}"
by (auto simp: rel_frontier_eq_empty affine_bounded_eq_lowdim [of T])
then obtain t where t: "t ∈ rel_frontier T" by auto
have ple: "int p ≤ aff_dim T" using Suc.prems by force
obtain h where conth: "continuous_on (⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p})) h"
and him: "h ` (⋃ (𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p}))
⊆ rel_frontier T"
and heq: "⋀x. x ∈ ⋃𝒢 ⟹ h x = f x"
using Suc.IH [OF ple] by auto
let ?Faces = "{D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D ≤ p}"
have extendh: "∃g. continuous_on D g ∧
g ` D ⊆ rel_frontier T ∧
(∀x ∈ D ∩ ⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p}). g x = h x)"
if D: "D ∈ 𝒢 ∪ ?Faces" for D
proof (cases "D ⊆ ⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p})")
case True
have "continuous_on D h"
using True conth continuous_on_subset by blast
moreover have "h ` D ⊆ rel_frontier T"
using True him by blast
ultimately show ?thesis
by blast
next
case False
note notDsub = False
show ?thesis
proof (cases "∃a. D = {a}")
case True
then obtain a where "D = {a}" by auto
with notDsub t show ?thesis
by (rule_tac x="λx. t" in exI) simp
next
case False
have "D ≠ {}" using notDsub by auto
have Dnotin: "D ∉ 𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p}"
using notDsub by auto
then have "D ∉ 𝒢" by simp
have "D ∈ ?Faces - {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p}"
using Dnotin that by auto
then obtain C where "C ∈ ℱ" "D face_of C" and affD: "aff_dim D = int p"
by auto
then have "bounded D"
using face_of_polytope_polytope poly polytope_imp_bounded by blast
then have [simp]: "¬ affine D"
using affine_bounded_eq_trivial False ‹D ≠ {}› ‹bounded D› by blast
have "{F. F facet_of D} ⊆ {E. E face_of C ∧ aff_dim E < int p}"
by clarify (metis ‹D face_of C› affD eq_iff face_of_trans facet_of_def zle_diff1_eq)
moreover have "polyhedron D"
using ‹C ∈ ℱ› ‹D face_of C› face_of_polytope_polytope poly polytope_imp_polyhedron by auto
ultimately have relf_sub: "rel_frontier D ⊆ ⋃ {E. E face_of C ∧ aff_dim E < p}"
then have him_relf: "h ∈ rel_frontier D → rel_frontier T"
using ‹C ∈ ℱ› him by blast
have "convex D"
by (simp add: ‹polyhedron D› polyhedron_imp_convex)
have affD_lessT: "aff_dim D < aff_dim T"
using Suc.prems affD by linarith
have contDh: "continuous_on (rel_frontier D) h"
using ‹C ∈ ℱ› relf_sub by (blast intro: continuous_on_subset [OF conth])
then have *: "(∃c. homotopic_with_canon (λx. True) (rel_frontier D) (rel_frontier T) h (λx. c)) =
(∃g. continuous_on UNIV g ∧  range g ⊆ rel_frontier T ∧
(∀x∈rel_frontier D. g x = h x))"
by (simp add: assms image_subset_iff_funcset rel_frontier_eq_empty him_relf nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier])
have "∃c. homotopic_with_canon (λx. True) (rel_frontier D) (rel_frontier T) h (λx. c)"
by (metis inessential_spheremap_lowdim_gen
[OF ‹convex D› ‹bounded D› ‹convex T› ‹bounded T› affD_lessT contDh him_relf])
then obtain g where contg: "continuous_on UNIV g"
and gim: "range g ⊆ rel_frontier T"
and gh: "⋀x. x ∈ rel_frontier D ⟹ g x = h x"
by (metis *)
have "D ∩ E ⊆ rel_frontier D"
if "E ∈ 𝒢 ∪ {D. Bex ℱ ((face_of) D) ∧ aff_dim D < int p}" for E
proof (rule face_of_subset_rel_frontier)
show "D ∩ E face_of D"
using that
proof safe
assume "E ∈ 𝒢"
then show "D ∩ E face_of D"
by (meson ‹C ∈ ℱ› ‹D face_of C› assms(2) face' face_of_Int_subface face_of_refl_eq poly polytope_imp_convex subsetD)
next
fix x
assume "aff_dim E < int p" "x ∈ ℱ" "E face_of x"
then show "D ∩ E face_of D"
by (meson ‹C ∈ ℱ› ‹D face_of C› face' face_of_Int_subface that)
qed
show "D ∩ E ≠ D"
using that notDsub by auto
qed
moreover have "continuous_on D g"
using contg continuous_on_subset by blast
ultimately show ?thesis
by (rule_tac x=g in exI) (use gh gim in fastforce)
qed
qed
have intle: "i < 1 + int j ⟷ i ≤ int j" for i j
by auto
have "finite 𝒢"
using ‹finite ℱ› ‹𝒢 ⊆ ℱ› rev_finite_subset by blast
moreover have "finite (?Faces)"
proof -
have §: "finite (⋃ {{D. D face_of C} |C. C ∈ ℱ})"
by (auto simp: ‹finite ℱ› finite_polytope_faces poly)
show ?thesis
by (auto intro: finite_subset [OF _ §])
qed
ultimately have fin: "finite (𝒢 ∪ ?Faces)"
by simp
have clo: "closed S" if "S ∈ 𝒢 ∪ ?Faces" for S
using that ‹𝒢 ⊆ ℱ› face_of_polytope_polytope poly polytope_imp_closed by blast
have K: "X ∩ Y ⊆ ⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < int p})"
if "X ∈ 𝒢 ∪ ?Faces" "Y ∈ 𝒢 ∪ ?Faces" "¬ Y ⊆ X" for X Y
proof -
have ff: "X ∩ Y face_of X ∧ X ∩ Y face_of Y"
if XY: "X face_of D" "Y face_of E" and DE: "D ∈ ℱ" "E ∈ ℱ" for D E
by (rule face_of_Int_subface [OF _ _ XY]) (auto simp: face' DE)
show ?thesis
using that
apply clarsimp
by (smt (verit, ccfv_SIG) IntI face_of_aff_dim_lt face_of_imp_convex [of X] face_of_imp_convex [of Y] face_of_trans ff)
qed
obtain g where "continuous_on (⋃(𝒢 ∪ ?Faces)) g"
"g ` ⋃(𝒢 ∪ ?Faces) ⊆ rel_frontier T"
"(∀x ∈ ⋃(𝒢 ∪ ?Faces) ∩
⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < p}). g x = h x)"
by (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+)
then show ?case
by (simp add: intle local.heq [symmetric], blast)
qed
have eq: "⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < i}) = ⋃ℱ"
proof
show "⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < int i}) ⊆ ⋃ℱ"
using ‹𝒢 ⊆ ℱ› face_of_imp_subset by fastforce
show "⋃ℱ ⊆ ⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < i})"
proof (rule Union_mono)
show "ℱ ⊆ 𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < int i}"
using face by (fastforce simp: aff i)
qed
qed
have "int i ≤ aff_dim T" by (simp add: i)
then show ?thesis
using extendf [of i] unfolding eq by (metis that)
qed

lemma extend_map_lemma_cofinite0:
assumes "finite ℱ"
and "pairwise (λS T. S ∩ T ⊆ K) ℱ"
and "⋀S. S ∈ ℱ ⟹ ∃a g. a ∉ U ∧ continuous_on (S - {a}) g ∧ g ` (S - {a}) ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)"
and "⋀S. S ∈ ℱ ⟹ closed S"
shows "∃C g. finite C ∧ disjnt C U ∧ card C ≤ card ℱ ∧
continuous_on (⋃ℱ - C) g ∧ g ` (⋃ℱ - C) ⊆ T
∧ (∀x ∈ (⋃ℱ - C) ∩ K. g x = h x)"
using assms
proof induction
case empty then show ?case
by force
next
case (insert X ℱ)
then have "closed X" and clo: "⋀X. X ∈ ℱ ⟹ closed X"
and ℱ: "⋀S. S ∈ ℱ ⟹ ∃a g. a ∉ U ∧ continuous_on (S - {a}) g ∧ g ` (S - {a}) ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)"
and pwX: "⋀Y. Y ∈ ℱ ∧ Y ≠ X ⟶ X ∩ Y ⊆ K ∧ Y ∩ X ⊆ K"
and pwF: "pairwise (λ S T. S ∩ T ⊆ K) ℱ"
obtain C g where C: "finite C" "disjnt C U" "card C ≤ card ℱ"
and contg: "continuous_on (⋃ℱ - C) g"
and gim: "g ` (⋃ℱ - C) ⊆ T"
and gh:  "⋀x. x ∈ (⋃ℱ - C) ∩ K ⟹ g x = h x"
using insert.IH [OF pwF ℱ clo] by auto
obtain a f where "a ∉ U"
and contf: "continuous_on (X - {a}) f"
and fim: "f ` (X - {a}) ⊆ T"
and fh: "(∀x ∈ X ∩ K. f x = h x)"
using insert.prems by (meson insertI1)
show ?case
proof (intro exI conjI)
show "finite (insert a C)"
show "disjnt (insert a C) U"
using C ‹a ∉ U› by simp
show "card (insert a C) ≤ card (insert X ℱ)"
by (simp add: C card_insert_if insert.hyps le_SucI)
have "closed (⋃ℱ)"
using clo insert.hyps by blast
have "continuous_on (X - insert a C) f"
using contf by (force simp: elim: continuous_on_subset)
moreover have "continuous_on (⋃ ℱ - insert a C) g"
using contg by (force simp: elim: continuous_on_subset)
ultimately
have "continuous_on (X - insert a C ∪ (⋃ℱ - insert a C)) (λx. if x ∈ X then f x else g x)"
apply (intro continuous_on_cases_local; simp add: closedin_closed)
using ‹closed X› apply blast
using ‹closed (⋃ℱ)› apply blast
using fh gh insert.hyps pwX by fastforce
then show "continuous_on (⋃(insert X ℱ) - insert a C) (λa. if a ∈ X then f a else g a)"
by (blast intro: continuous_on_subset)
show "∀x∈(⋃(insert X ℱ) - insert a C) ∩ K. (if x ∈ X then f x else g x) = h x"
using gh by (auto simp: fh)
show "(λa. if a ∈ X then f a else g a) ` (⋃(insert X ℱ) - insert a C) ⊆ T"
using fim gim by auto force
qed
qed

lemma extend_map_lemma_cofinite1:
assumes "finite ℱ"
and ℱ: "⋀X. X ∈ ℱ ⟹ ∃a g. a ∉ U ∧ continuous_on (X - {a}) g ∧ g ` (X - {a}) ⊆ T ∧ (∀x ∈ X ∩ K. g x = h x)"
and clo: "⋀X. X ∈ ℱ ⟹ closed X"
and K: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ; ¬ X ⊆ Y; ¬ Y ⊆ X⟧ ⟹ X ∩ Y ⊆ K"
obtains C g where "finite C" "disjnt C U" "card C ≤ card ℱ" "continuous_on (⋃ℱ - C) g"
"g ` (⋃ℱ - C) ⊆ T"
"⋀x. x ∈ (⋃ℱ - C) ∩ K ⟹ g x = h x"
proof -
let ?ℱ = "{X ∈ ℱ. ∀Y∈ℱ. ¬ X ⊂ Y}"
have [simp]: "⋃?ℱ = ⋃ℱ"
have fin: "finite ?ℱ"
by (force intro: finite_subset [OF _ ‹finite ℱ›])
have pw: "pairwise (λ S T. S ∩ T ⊆ K) ?ℱ"
by (simp add: pairwise_def) (metis K psubsetI)
have "card {X ∈ ℱ. ∀Y∈ℱ. ¬ X ⊂ Y} ≤ card ℱ"
by (simp add: ‹finite ℱ› card_mono)
moreover
obtain C g where "finite C ∧ disjnt C U ∧ card C ≤ card ?ℱ ∧
continuous_on (⋃?ℱ - C) g ∧ g ` (⋃?ℱ - C) ⊆ T
∧ (∀x ∈ (⋃?ℱ - C) ∩ K. g x = h x)"
using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo ℱ)
ultimately show ?thesis
by (rule_tac C=C and g=g in that) auto
qed

lemma extend_map_lemma_cofinite:
assumes "finite ℱ" "𝒢 ⊆ ℱ" and T: "convex T" "bounded T"
and poly: "⋀X. X ∈ ℱ ⟹ polytope X"
and contf: "continuous_on (⋃𝒢) f" and fim: "f ` (⋃𝒢) ⊆ rel_frontier T"
and face: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ (X ∩ Y) face_of X"
and aff: "⋀X. X ∈ ℱ - 𝒢 ⟹ aff_dim X ≤ aff_dim T"
obtains C g where
"finite C" "disjnt C (⋃𝒢)" "card C ≤ card ℱ" "continuous_on (⋃ℱ - C) g"
"g ` (⋃ ℱ - C) ⊆ rel_frontier T" "⋀x. x ∈ ⋃𝒢 ⟹ g x = f x"
proof -
define ℋ where "ℋ ≡ 𝒢 ∪ {D. ∃C ∈ ℱ - 𝒢. D face_of C ∧ aff_dim D < aff_dim T}"
have "finite 𝒢"
using assms finite_subset by blast
have *: "finite (⋃{{D. D face_of C} |C. C ∈ ℱ})"
using finite_polytope_faces poly ‹finite ℱ› by force
then have "finite ℋ"
by (auto simp: ℋ_def ‹finite 𝒢› intro: finite_subset [OF _ *])
have face': "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ⟧ ⟹ (S ∩ T) face_of S ∧ (S ∩ T) face_of T"
by (metis face inf_commute)
have *: "⋀X Y. ⟦X ∈ ℋ; Y ∈ ℋ⟧ ⟹ X ∩ Y face_of X"
by (simp add: ℋ_def) (smt (verit) ‹𝒢 ⊆ ℱ› DiffE face' face_of_Int_subface in_mono inf.idem)
obtain h where conth: "continuous_on (⋃ℋ) h" and him: "h ` (⋃ℋ) ⊆ rel_frontier T"
and hf: "⋀x. x ∈ ⋃𝒢 ⟹ h x = f x"
proof (rule extend_map_lemma [OF ‹finite ℋ› [unfolded ℋ_def] Un_upper1 T])
show "⋀X. ⟦X ∈ 𝒢 ∪ {D. ∃C∈ℱ - 𝒢. D face_of C ∧ aff_dim D < aff_dim T}⟧ ⟹ polytope X"
using ‹𝒢 ⊆ ℱ› face_of_polytope_polytope poly by fastforce
qed (use * ℋ_def contf fim in auto)
have "bounded (⋃𝒢)"
using ‹finite 𝒢› ‹𝒢 ⊆ ℱ› poly polytope_imp_bounded by blast
then have "⋃𝒢 ≠ UNIV"
by auto
then obtain a where a: "a ∉ ⋃𝒢"
by blast
have ℱ: "∃a g. a ∉ ⋃𝒢 ∧ continuous_on (D - {a}) g ∧
g ` (D - {a}) ⊆ rel_frontier T ∧ (∀x ∈ D ∩ ⋃ℋ. g x = h x)"
if "D ∈ ℱ" for D
proof (cases "D ⊆ ⋃ℋ")
case True
then have "h ` (D - {a}) ⊆ rel_frontier T" "continuous_on (D - {a}) h"
using him by (blast intro!: ‹a ∉ ⋃𝒢› continuous_on_subset [OF conth])+
then show ?thesis
using a by blast
next
case False
note D_not_subset = False
show ?thesis
proof (cases "D ∈ 𝒢")
case True
with D_not_subset show ?thesis
by (auto simp: ℋ_def)
next
case False
then have affD: "aff_dim D ≤ aff_dim T"
by (simp add: ‹D ∈ ℱ› aff)
show ?thesis
proof (cases "rel_interior D = {}")
case True
with ‹D ∈ ℱ› poly a show ?thesis
by (force simp: rel_interior_eq_empty polytope_imp_convex)
next
case False
then obtain b where brelD: "b ∈ rel_interior D"
by blast
have "polyhedron D"
by (simp add: poly polytope_imp_polyhedron that)
have "rel_frontier D retract_of affine hull D - {b}"
by (simp add: rel_frontier_retract_of_punctured_affine_hull poly polytope_imp_bounded polytope_imp_convex that brelD)
then obtain r where relfD: "rel_frontier D ⊆ affine hull D - {b}"
and contr: "continuous_on (affine hull D - {b}) r"
and rim: "r ` (affine hull D - {b}) ⊆ rel_frontier D"
and rid: "⋀x. x ∈ rel_frontier D ⟹ r x = x"
by (auto simp: retract_of_def retraction_def)
show ?thesis
proof (intro exI conjI ballI)
show "b ∉ ⋃𝒢"
proof clarify
fix E
assume "b ∈ E" "E ∈ 𝒢"
then have "E ∩ D face_of E ∧ E ∩ D face_of D"
using ‹𝒢 ⊆ ℱ› face' that by auto
with face_of_subset_rel_frontier ‹E ∈ 𝒢› ‹b ∈ E› brelD rel_interior_subset [of D]
D_not_subset rel_frontier_def ℋ_def
show False
by blast
qed
have "r ` (D - {b}) ⊆ r ` (affine hull D - {b})"
by (simp add: Diff_mono hull_subset image_mono)
also have "... ⊆ rel_frontier D"
by (rule rim)
also have "... ⊆ ⋃{E. E face_of D ∧ aff_dim E < aff_dim T}"
using affD
by (force simp: rel_frontier_of_polyhedron [OF ‹polyhedron D›] facet_of_def)
also have "... ⊆ ⋃(ℋ)"
using D_not_subset ℋ_def that by fastforce
finally have rsub: "r ` (D - {b}) ⊆ ⋃(ℋ)" .
show "continuous_on (D - {b}) (h ∘ r)"
proof (rule continuous_on_compose)
show "continuous_on (D - {b}) r"
by (meson Diff_mono continuous_on_subset contr hull_subset order_refl)
show "continuous_on (r ` (D - {b})) h"
by (simp add: Diff_mono hull_subset continuous_on_subset [OF conth rsub])
qed
show "(h ∘ r) ` (D - {b}) ⊆ rel_frontier T"
using brelD him rsub by fastforce
show "(h ∘ r) x = h x" if x: "x ∈ D ∩ ⋃ℋ" for x
proof -
consider A where "x ∈ D" "A ∈ 𝒢" "x ∈ A"
| A B where "x ∈ D" "A face_of B" "B ∈ ℱ" "B ∉ 𝒢" "aff_dim A < aff_dim T" "x ∈ A"
using x by (auto simp: ℋ_def)
then have xrel: "x ∈ rel_frontier D"
proof cases
case 1 show ?thesis
proof (rule face_of_subset_rel_frontier [THEN subsetD])
show "D ∩ A face_of D"
using ‹A ∈ 𝒢› ‹𝒢 ⊆ ℱ› face ‹D ∈ ℱ› by blast
show "D ∩ A ≠ D"
using ‹A ∈ 𝒢› D_not_subset ℋ_def by blast
qed (auto simp: 1)
next
case 2 show ?thesis
proof (rule face_of_subset_rel_frontier [THEN subsetD])
have "D face_of D"
by (simp add: ‹polyhedron D› polyhedron_imp_convex face_of_refl)
then show "D ∩ A face_of D"
by (meson "2"(2) "2"(3) ‹D ∈ ℱ› face' face_of_Int_Int face_of_face)
show "D ∩ A ≠ D"
using "2" D_not_subset ℋ_def by blast
qed (auto simp: 2)
qed
show ?thesis
qed
qed
qed
qed
qed
have clo: "⋀S. S ∈ ℱ ⟹ closed S"
obtain C g where "finite C" "disjnt C (⋃𝒢)" "card C ≤ card ℱ" "continuous_on (⋃ℱ - C) g"
"g ` (⋃ℱ - C) ⊆ rel_frontier T"
and gh: "⋀x. x ∈ (⋃ℱ - C) ∩ ⋃ℋ ⟹ g x = h x"
proof (rule extend_map_lemma_cofinite1 [OF ‹finite ℱ› ℱ clo])
show "X ∩ Y ⊆ ⋃ℋ" if XY: "X ∈ ℱ" "Y ∈ ℱ" and "¬ X ⊆ Y" "¬ Y ⊆ X" for X Y
proof (cases "X ∈ 𝒢")
case True
then show ?thesis
by (auto simp: ℋ_def)
next
case False
have "X ∩ Y ≠ X"
using ‹¬ X ⊆ Y› by blast
with XY
show ?thesis
by (clarsimp simp: ℋ_def)
(metis Diff_iff Int_iff aff antisym_conv face face_of_aff_dim_lt face_of_refl
not_le poly polytope_imp_convex)
qed
qed (blast)+
with ‹𝒢 ⊆ ℱ› show ?thesis
by (rule_tac C=C and g=g in that) (auto simp: disjnt_def hf [symmetric] ℋ_def intro!: gh)
qed

text‹The next two proofs are similar›
theorem extend_map_cell_complex_to_sphere:
assumes "finite ℱ" and S: "S ⊆ ⋃ℱ" "closed S" and T: "convex T" "bounded T"
and poly: "⋀X. X ∈ ℱ ⟹ polytope X"
and aff: "⋀X. X ∈ ℱ ⟹ aff_dim X < aff_dim T"
and face: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ (X ∩ Y) face_of X"
and contf: "continuous_on S f" and fim: "f ∈ S → rel_frontier T"
obtains g where "continuous_on (⋃ℱ) g"
"g ` (⋃ℱ) ⊆ rel_frontier T" "⋀x. x ∈ S ⟹ g x = f x"
proof -
obtain V g where "S ⊆ V" "open V" "continuous_on V g" and gim: "g ∈ V → rel_frontier T" and gf: "⋀x. x ∈ S ⟹ g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ ‹closed S›] ANR_rel_frontier_convex T by blast
have "compact S"
by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact)
then obtain d where "d > 0" and d: "⋀x y. ⟦x ∈ S; y ∈ - V⟧ ⟹ d ≤ dist x y"
using separate_compact_closed [of S "-V"] ‹open V› ‹S ⊆ V› by force
obtain 𝒢 where "finite 𝒢" "⋃𝒢 = ⋃ℱ"
and diaG: "⋀X. X ∈ 𝒢 ⟹ diameter X < d"
and polyG: "⋀X. X ∈ 𝒢 ⟹ polytope X"
and affG: "⋀X. X ∈ 𝒢 ⟹ aff_dim X ≤ aff_dim T - 1"
and faceG: "⋀X Y. ⟦X ∈ 𝒢; Y ∈ 𝒢⟧ ⟹ X ∩ Y face_of X"
proof (rule cell_complex_subdivision_exists [OF ‹d>0› ‹finite ℱ› poly _ face])
show "⋀X. X ∈ ℱ ⟹ aff_dim X ≤ aff_dim T - 1"
qed auto
obtain h where conth: "continuous_on (⋃𝒢) h" and him: "h ` ⋃𝒢 ⊆ rel_frontier T" and hg: "⋀x. x ∈ ⋃(𝒢 ∩ Pow V) ⟹ h x = g x"
proof (rule extend_map_lemma [of 𝒢 "𝒢 ∩ Pow V" T g])
show "continuous_on (⋃(𝒢 ∩ Pow V)) g"
by (metis Union_Int_subset Union_Pow_eq ‹continuous_on V g› continuous_on_subset le_inf_iff)
qed (use ‹finite 𝒢› T polyG affG faceG gim in fastforce)+
show ?thesis
proof
show "continuous_on (⋃ℱ) h"
using ‹⋃𝒢 = ⋃ℱ› conth by auto
show "h ` ⋃ℱ ⊆ rel_frontier T"
using ‹⋃𝒢 = ⋃ℱ› him by auto
show "h x = f x" if "x ∈ S" for x
proof -
have "x ∈ ⋃𝒢"
using ‹⋃𝒢 = ⋃ℱ› ‹S ⊆ ⋃ℱ› that by auto
then obtain X where "x ∈ X" "X ∈ 𝒢" by blast
then have "diameter X < d" "bounded X"
by (auto simp: diaG ‹X ∈ 𝒢› polyG polytope_imp_bounded)
then have "X ⊆ V" using d [OF ‹x ∈ S›] diameter_bounded_bound [OF ‹bounded X› ‹x ∈ X›]
by fastforce
have "h x = g x"
using ‹X ∈ 𝒢› ‹X ⊆ V› ‹x ∈ X› hg by auto
also have "... = f x"
finally show "h x = f x" .
qed
qed
qed

theorem extend_map_cell_complex_to_sphere_cofinite:
assumes "finite ℱ" and S: "S ⊆ ⋃ℱ" "closed S" and T: "convex T" "bounded T"
and poly: "⋀X. X ∈ ℱ ⟹ polytope X"
and aff: "⋀X. X ∈ ℱ ⟹ aff_dim X ≤ aff_dim T"
and face: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ (X ∩ Y) face_of X"
and contf: "continuous_on S f" and fim: "f ∈ S → rel_frontier T"
obtains C g where "finite C" "disjnt C S" "continuous_on (⋃ℱ - C) g"
"g ` (⋃ℱ - C) ⊆ rel_frontier T" "⋀x. x ∈ S ⟹ g x = f x"
proof -
obtain V g where "S ⊆ V" "open V" "continuous_on V g" and gim: "g ∈ V → rel_frontier T" and gf: "⋀x. x ∈ S ⟹ g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ ‹closed S›] ANR_rel_frontier_convex T by blast
have "compact S"
by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact)
then obtain d where "d > 0" and d: "⋀x y. ⟦x ∈ S; y ∈ - V⟧ ⟹ d ≤ dist x y"
using separate_compact_closed [of S "-V"] ‹open V› ‹S ⊆ V› by force
obtain 𝒢 where "finite 𝒢" "⋃𝒢 = ⋃ℱ"
and diaG: "⋀X. X ∈ 𝒢 ⟹ diameter X < d"
and polyG: "⋀X. X ∈ 𝒢 ⟹ polytope X"
and affG: "⋀X. X ∈ 𝒢 ⟹ aff_dim X ≤ aff_dim T"
and faceG: "⋀X Y. ⟦X ∈ 𝒢; Y ∈ 𝒢⟧ ⟹ X ∩ Y face_of X"
by (rule cell_complex_subdivision_exists [OF ‹d>0› ‹finite ℱ› poly aff face]) auto
obtain C h where "finite C" and dis: "disjnt C (⋃(𝒢 ∩ Pow V))"
and card: "card C ≤ card 𝒢" and conth: "continuous_on (⋃𝒢 - C) h"
and him: "h ` (⋃𝒢 - C) ⊆ rel_frontier T"
and hg: "⋀x. x ∈ ⋃(𝒢 ∩ Pow V) ⟹ h x = g x"
proof (rule extend_map_lemma_cofinite [of 𝒢 "𝒢 ∩ Pow V" T g])
show "continuous_on (⋃(𝒢 ∩ Pow V)) g"
by (metis Union_Int_subset Union_Pow_eq ‹continuous_on V g› continuous_on_subset le_inf_iff)
show "g ` ⋃(𝒢 ∩ Pow V) ⊆ rel_frontier T"
using gim by force
qed (auto intro: ‹finite 𝒢› T polyG affG dest: faceG)
have Ssub: "S ⊆ ⋃(𝒢 ∩ Pow V)"
proof
fix x
assume "x ∈ S"
then have "x ∈ ⋃𝒢"
using ‹⋃𝒢 = ⋃ℱ› ‹S ⊆ ⋃ℱ› by auto
then obtain X where "x ∈ X" "X ∈ 𝒢" by blast
then have "diameter X < d" "bounded X"
by (auto simp: diaG ‹X ∈ 𝒢› polyG polytope_imp_bounded)
then have "X ⊆ V" using d [OF ‹x ∈ S›] diameter_bounded_bound [OF ‹bounded X› ‹x ∈ X›]
by fastforce
then show "x ∈ ⋃(𝒢 ∩ Pow V)"
using ‹X ∈ 𝒢› ‹x ∈ X› by blast
qed
show ?thesis
proof
show "continuous_on (⋃ℱ-C) h"
using ‹⋃𝒢 = ⋃ℱ› conth by auto
show "h ` (⋃ℱ - C) ⊆ rel_frontier T"
using ‹⋃𝒢 = ⋃ℱ› him by auto
show "h x = f x" if "x ∈ S" for x
proof -
have "h x = g x"
using Ssub hg that by blast
also have "... = f x"
finally show "h x = f x" .
qed
show "disjnt C S"
using dis Ssub  by (meson disjnt_iff subset_eq)
qed (intro ‹finite C›)
qed

subsection‹ Special cases and corollaries involving spheres›

proposition extend_map_affine_to_sphere_cofinite_simple:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "compact S" "convex U" "bounded U"
and aff: "aff_dim T ≤ aff_dim U"
and "S ⊆ T" and contf: "continuous_on S f"
and fim: "f ∈ S → rel_frontier U"
obtains K g where "finite K" "K ⊆ T" "disjnt K S" "continuous_on (T - K) g"
"g ∈ (T - K) → rel_frontier U"
"⋀x. x ∈ S ⟹ g x = f x"
proof -
have "∃K g. finite K ∧ disjnt K S ∧ continuous_on (T - K) g ∧
g ∈ (T - K) → rel_frontier U ∧ (∀x ∈ S. g x = f x)"
if "affine T" "S ⊆ T" and aff: "aff_dim T ≤ aff_dim U"  for T
proof (cases "S = {}")
case True
show ?thesis
proof (cases "rel_frontier U = {}")
case True
with ‹bounded U› have "aff_dim U ≤ 0"
using affine_bounded_eq_lowdim rel_frontier_eq_empty by auto
with aff have "aff_dim T ≤ 0" by auto
then obtain a where "T ⊆ {a}"
using ‹affine T› affine_bounded_eq_lowdim affine_bounded_eq_trivial by auto
then show ?thesis
using ‹S = {}› fim
by (metis Diff_cancel contf disjnt_empty2 finite.emptyI finite_insert finite_subset)
next
case False
then obtain a where "a ∈ rel_frontier U"
by auto
then show ?thesis
using continuous_on_const [of _ a] ‹S = {}› by force
qed
next
case False
have "bounded S"
by (simp add: ‹compact S› compact_imp_bounded)
then obtain b where b: "S ⊆ cbox (-b) b"
using bounded_subset_cbox_symmetric by blast
define bbox where "bbox ≡ cbox (-(b+One)) (b+One)"
have "cbox (-b) b ⊆ bbox"
by (auto simp: bbox_def algebra_simps intro!: subset_box_imp)
with b ‹S ⊆ T› have "S ⊆ bbox ∩ T"
by auto
then have Ssub: "S ⊆ ⋃{bbox ∩ T}"
by auto
then have "aff_dim (bbox ∩ T) ≤ aff_dim U"
by (metis aff aff_dim_subset inf_commute inf_le1 order_trans)
obtain K g where K: "finite K" "disjnt K S"
and contg: "continuous_on (⋃{bbox ∩ T} - K) g"
and gim: "g ` (⋃{bbox ∩ T} - K) ⊆ rel_frontier U"
and gf: "⋀x. x ∈ S ⟹ g x = f x"
proof (rule extend_map_cell_complex_to_sphere_cofinite
[OF _ Ssub _ ‹convex U› ‹bounded U› _ _ _ contf fim])
show "closed S"
using ‹compact S› compact_eq_bounded_closed by auto
show poly: "⋀X. X ∈ {bbox ∩ T} ⟹ polytope X"
by (simp add: polytope_Int_polyhedron bbox_def polytope_interval affine_imp_polyhedron ‹affine T›)
show "⋀X Y. ⟦X ∈ {bbox ∩ T}; Y ∈ {bbox ∩ T}⟧ ⟹ X ∩ Y face_of X"
show "⋀X. X ∈ {bbox ∩ T} ⟹ aff_dim X ≤ aff_dim U"
by (simp add: ‹aff_dim (bbox ∩ T) ≤ aff_dim U›)
qed auto
define fro where "fro ≡ λd. frontier(cbox (-(b + d *⇩R One)) (b + d *⇩R One))"
obtain d where d12: "1/2 ≤ d" "d ≤ 1" and dd: "disjnt K (fro d)"
proof (rule disjoint_family_elem_disjnt [OF _ ‹finite K›])
show "infinite {1/2..1::real}"
have dis1: "disjnt (fro x) (fro y)" if "x<y" for x y
by (auto simp: algebra_simps that subset_box_imp disjnt_Diff1 frontier_def fro_def)
then show "disjoint_family_on fro {1/2..1}"
by (auto simp: disjoint_family_on_def disjnt_def neq_iff)
qed auto
define c where "c ≡ b + d *⇩R One"
have cbsub: "cbox (-b) b ⊆ box (-c) c" "cbox (-b) b ⊆ cbox (-c) c"  "cbox (-c) c ⊆ bbox"
using d12 by (auto simp: algebra_simps subset_box_imp c_def bbox_def)
have clo_cbT: "closed (cbox (- c) c ∩ T)"
by (simp add: affine_closed closed_Int closed_cbox ‹affine T›)
have cpT_ne: "cbox (- c) c ∩ T ≠ {}"
using ‹S ≠ {}› b cbsub(2) ‹S ⊆ T› by fastforce
have "closest_point (cbox (- c) c ∩ T) x ∉ K" if "x ∈ T" "x ∉ K" for x
proof (cases "x ∈ cbox (-c) c")
case True with that show ?thesis
next
case False
have int_ne: "interior (cbox (-c) c) ∩ T ≠ {}"
using ‹S ≠ {}› ‹S ⊆ T› b ‹cbox (- b) b ⊆ box (- c) c› by force
have "convex T"
by (meson ‹affine T› affine_imp_convex)
then have "x ∈ affine hull (cbox (- c) c ∩ T)"
by (metis Int_commute Int_iff ‹S ≠ {}› ‹S ⊆ T› cbsub(1) ‹x ∈ T› affine_hull_convex_Int_nonempty_interior all_not_in_conv b hull_inc inf.orderE interior_cbox)
then have "x ∈ affine hull (cbox (- c) c ∩ T) - rel_interior (cbox (- c) c ∩ T)"
by (meson DiffI False Int_iff rel_interior_subset subsetCE)
then have "closest_point (cbox (- c) c ∩ T) x ∈ rel_frontier (cbox (- c) c ∩ T)"
by (rule closest_point_in_rel_frontier [OF clo_cbT cpT_ne])
moreover have "(rel_frontier (cbox (- c) c ∩ T)) ⊆ fro d"
by (subst convex_affine_rel_frontier_Int [OF _  ‹affine T› int_ne]) (auto simp: fro_def c_def)
ultimately show ?thesis
using dd  by (force simp: disjnt_def)
qed
then have cpt_subset: "closest_point (cbox (- c) c ∩ T) ` (T - K) ⊆ ⋃{bbox ∩ T} - K"
using closest_point_in_set [OF clo_cbT cpT_ne] cbsub(3) by force
show ?thesis
proof (intro conjI ballI exI)
have "continuous_on (T - K) (closest_point (cbox (- c) c ∩ T))"
proof (rule continuous_on_closest_point)
show "convex (cbox (- c) c ∩ T)"
by (simp add: affine_imp_convex convex_Int ‹affine T›)
show "closed (cbox (- c) c ∩ T)"
using clo_cbT by blast
show "cbox (- c) c ∩ T ≠ {}"
using ‹S ≠ {}› cbsub(2) b that by auto
qed
then show "continuous_on (T - K) (g ∘ closest_point (cbox (- c) c ∩ T))"
by (metis continuous_on_compose continuous_on_subset [OF contg cpt_subset])
have "(g ∘ closest_point (cbox (- c) c ∩ T)) ` (T - K) ⊆ g ` (⋃{bbox ∩ T} - K)"
by (metis image_comp image_mono cpt_subset)
also have "... ⊆ rel_frontier U"
by (rule gim)
finally show "(g ∘ closest_point (cbox (- c) c ∩ T)) ∈ (T - K) → rel_frontier U"
by blast
show "(g ∘ closest_point (cbox (- c) c ∩ T)) x = f x" if "x ∈ S" for x
proof -
have "(g ∘ closest_point (cbox (- c) c ∩ T)) x = g x"
unfolding o_def
by (metis IntI ‹S ⊆ T› b cbsub(2) closest_point_self subset_eq that)
also have "... = f x"
finally show ?thesis .
qed
qed (auto simp: K)
qed
then obtain K g where "finite K" "disjnt K S"
and contg: "continuous_on (affine hull T - K) g"
and gim:  "g ∈ (affine hull T - K) → rel_frontier U"
and gf:   "⋀x. x ∈ S ⟹ g x = f x"
by (metis aff affine_affine_hull aff_dim_affine_hull
order_trans [OF ‹S ⊆ T› hull_subset [of T affine]])
then obtain K g where "finite K" "disjnt K S"
and contg: "continuous_on (T - K) g"
and gim:  "g ` (T - K) ⊆ rel_frontier U"
and gf:   "⋀x. x ∈ S ⟹ g x = f x"
by (rule_tac K=K and g=g in that) (auto simp: hull_inc elim: continuous_on_subset)
then show ?thesis
by (rule_tac K="K ∩ T" and g=g in that) (auto simp: disjnt_iff Diff_Int contg)
qed

subsection‹Extending maps to spheres›

(*Up to extend_map_affine_to_sphere_cofinite_gen*)

lemma extend_map_affine_to_sphere1:
fixes f :: "'a::euclidean_space ⇒ 'b::topological_space"
assumes "finite K" "affine U" and contf: "continuous_on (U - K) f"
and fim: "f ∈ (U - K) → T"
and comps: "⋀C. ⟦C ∈ components(U - S); C ∩ K ≠ {}⟧ ⟹ C ∩ L ≠ {}"
and clo: "closedin (top_of_set U) S" and K: "disjnt K S" "K ⊆ U"
obtains g where "continuous_on (U - L) g" "g ∈ (U - L) → T" "⋀x. x ∈ S ⟹ g x = f x"
proof (cases "K = {}")
case True
then show ?thesis
by (metis DiffD1 Diff_empty Diff_subset PiE Pi_I contf continuous_on_subset fim that)
next
case False
have "S ⊆ U"
using clo closedin_limpt by blast
then have "(U - S) ∩ K ≠ {}"
by (metis Diff_triv False Int_Diff K disjnt_def inf.absorb_iff2 inf_commute)
then have "⋃(components (U - S)) ∩ K ≠ {}"
using Union_components by simp
then obtain C0 where C0: "C0 ∈ components (U - S)" "C0 ∩ K ≠ {}"
by blast
have "convex U"
by (simp add: affine_imp_convex ‹affine U›)
then have "locally connected U"
by (rule convex_imp_locally_connected)
have "∃a g. a ∈ C ∧ a ∈ L ∧ continuous_on (S ∪ (C - {a})) g ∧
g ` (S ∪ (C - {a})) ⊆ T ∧ (∀x ∈ S. g x = f x)"
if C: "C ∈ components (U - S)" and CK: "C ∩ K ≠ {}" for C
proof -
have "C ⊆ U-S" "C ∩ L ≠ {}"
by (simp_all add: in_components_subset comps that)
then obtain a where a: "a ∈ C" "a ∈ L" by auto
have opeUC: "openin (top_of_set U) C"
by (m```