From 2a87489fb9c5ed0c2be8f7a86127270d9ec94dc3 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Wed, 6 Dec 2023 17:33:22 -0500 Subject: [PATCH] WIP --- SphereEversion/Global/Gromov.lean | 270 +++++++++++++++++--- SphereEversion/Global/LocalisationData.lean | 6 +- 2 files changed, 243 insertions(+), 33 deletions(-) diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean index a13d4a15..8cabeba9 100644 --- a/SphereEversion/Global/Gromov.lean +++ b/SphereEversion/Global/Gromov.lean @@ -33,6 +33,215 @@ variable {EM : Type _} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimen local notation "J¹" => OneJetBundle IM M IX X + +-- TODO: cleanup the following awful mess +lemma OpenEmbedding.homeomorph {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + {f : X → Y} (hf : OpenEmbedding f) : Homeomorph X (range f) where + toFun := rangeFactorization f + invFun := Function.surjInv surjective_onto_range + left_inv := by + apply Function.leftInverse_surjInv + exact ⟨fun x x' h ↦ hf.inj <| by simpa [rangeFactorization] using h, surjective_onto_range⟩ + right_inv := Function.rightInverse_surjInv surjective_onto_range + continuous_toFun := continuous_induced_rng.mpr hf.continuous + continuous_invFun := by + dsimp + refine continuous_def.mpr ?_ + intro U U_op + rw [← image_eq_preimage_of_inverse] + swap + apply Function.leftInverse_surjInv + exact ⟨fun x x' h ↦ hf.inj <| by simpa [rangeFactorization] using h, surjective_onto_range⟩ + rw [isOpen_induced_iff] + use f '' U, hf.isOpenMap U U_op + ext ⟨y, x, rfl⟩ + apply exists_congr + intro x' + apply and_congr Iff.rfl + conv_lhs => rw [← rangeFactorization_eq (f := f)] + erw [Subtype.val_inj] + rfl + exact Function.rightInverse_surjInv surjective_onto_range + + + +lemma OpenEmbedding.isCompact_preimage {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + {f : X → Y} (hf : OpenEmbedding f) {K : Set Y} (K_cpct: IsCompact K) (Kf : K ⊆ range f) : + IsCompact (f ⁻¹' K) := by + + let K' : Set (range f) := {x | (x : Y) ∈ K} + have K'_cpct : IsCompact K':= by + refine Subtype.isCompact_iff.mpr ?_ + convert K_cpct + change Subtype.val '' (Subtype.val ⁻¹' K) = K + sorry + convert hf.homeomorph.isCompact_preimage.mpr K'_cpct + ext x + change f x ∈ K ↔ ↑(hf.homeomorph x) ∈ K + unfold OpenEmbedding.homeomorph + simp only [Homeomorph.homeomorph_mk_coe, Equiv.coe_fn_mk, rangeFactorization_coe] + + +theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen R) (hA : IsClosed A) + (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) : R.SatisfiesHPrinciple A δ := by +borelize EX +letI := manifoldMetric IM M +haveI := locally_compact_manifold IM M +haveI := locally_compact_manifold IX X +refine' RelMfld.satisfiesHPrinciple_of_weak hA _ +clear! A +intro A hA 𝓕₀ h𝓕₀ +cases' isEmpty_or_nonempty M with hM hM +· refine' ⟨emptyHtpyFormalSol R, _, _, _, _⟩ + all_goals try apply eventually_of_forall _ + all_goals try intro + all_goals try intro + all_goals + first + | apply empty_htpy_formal_sol_eq + | apply (IsEmpty.false ‹M›).elim +cases' isEmpty_or_nonempty X with hX hX +· exfalso + inhabit M + exact (IsEmpty.false <| 𝓕₀.bs default).elim +-- We now start the main proof under the assumption that `M` and `X` are nonempty. +have cont : Continuous 𝓕₀.bs := 𝓕₀.smooth_bs.continuous +rcases exists_stability_dist IM IX cont with ⟨ε, ε_pos, ε_cont, hε⟩ +let τ := fun x : M ↦ min (δ x) (ε x) +have τ_pos : ∀ x, 0 < τ x := fun x ↦ lt_min (hδ_pos x) (ε_pos x) +have τ_cont : Continuous τ := hδ_cont.min ε_cont +have := fun (x : M) (F' : Germ (𝓝 x) J¹) ↦ F'.value = 𝓕₀ x +let P₀ : ∀ x : M, Germ (𝓝 x) J¹ → Prop := fun x F ↦ + F.value.1.1 = x ∧ + F.value ∈ R ∧ + F.ContMDiffAt' IM ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ ∧ + RestrictGermPredicate (fun x F' ↦ F'.value = 𝓕₀ x) A x F ∧ + dist F.value.1.2 (𝓕₀.bs x) < τ x +let P₁ : ∀ x : M, Germ (𝓝 x) J¹ → Prop := fun x F ↦ IsHolonomicGerm F +let P₂ : ∀ p : ℝ × M, Germ (𝓝 p) J¹ → Prop := fun p F ↦ + F.ContMDiffAt' (𝓘(ℝ).prod IM) ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ +have hP₂ : ∀ (a b : ℝ) (p : ℝ × M) (f : ℝ × M → J¹), + P₂ (a * p.1 + b, p.2) f → P₂ p fun p : ℝ × M ↦ f (a * p.1 + b, p.2) := by + sorry/- rintro a b ⟨t, x⟩ f h + change ContMDiffAt _ _ _ (f ∘ fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x) + change ContMDiffAt _ _ _ f ((fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x)) at h + have : + ContMDiffAt (𝓘(ℝ, ℝ).prod IM) (𝓘(ℝ, ℝ).prod IM) ∞ (fun p : ℝ × M ↦ (a * p.1 + b, p.2)) + (t, x) := + haveI h₁ : ContMDiffAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ∞ (fun t ↦ a * t + b) t := + contMDiffAt_iff_contDiffAt.mpr + (((contDiffAt_id : ContDiffAt ℝ ∞ id t).const_smul a).add contDiffAt_const) + h₁.prod_map contMDiffAt_id + exact h.comp (t, x) this -/ +have init : ∀ x : M, P₀ x (𝓕₀ : M → J¹) := + by + refine' fun x ↦ ⟨rfl, 𝓕₀.is_sol x, 𝓕₀.smooth x, _, _⟩ + · revert x + exact forall_restrictGermPredicate_of_forall fun x ↦ rfl + · erw [dist_self] + exact τ_pos x +have hP₂' : ∀ (t : ℝ) (x : M) (f : M → J¹), P₀ x f → P₂ (t, x) fun p : ℝ × M ↦ f p.2 := + sorry + +have ind : ∀ m : M, + ∃ V ∈ 𝓝 m, ∀ K₁ ⊆ V, ∀ K₀ ⊆ interior K₁, IsCompact K₀ → IsCompact K₁ → ∀ (C : Set M) (f : M → J¹), + IsClosed C → (∀ x, P₀ x f) → (∀ᶠ x in 𝓝ˢ C, P₁ x f) → + ∃ F : ℝ → M → J¹, (∀ t x, P₀ x (F t)) ∧ + (∀ᶠ x in 𝓝ˢ (C ∪ K₀), P₁ x (F 1)) ∧ + (∀ (p : ℝ × M), P₂ p ↿F) ∧ + (∀ t, ∀ x ∉ K₁, F t x = f x) ∧ + (∀ᶠ t in 𝓝ˢ (Iic 0), F t = f) ∧ + ∀ᶠ t in 𝓝ˢ (Ici 1), F t = F 1 := by + intro m + rcases hε m with ⟨φ, ψ, ⟨e, rfl⟩, hφψ⟩ + have : φ '' ball e 1 ∈ 𝓝 (φ e) := by + rw [← φ.openEmbedding.map_nhds_eq] + exact image_mem_map (ball_mem_nhds e zero_lt_one) + use φ '' (ball e 1), this ; clear this + intro K₁ hK₁ K₀ K₀K₁ K₀_cpct K₁_cpct C f C_closed P₀f fC + replace K₀_cpct : IsCompact (φ ⁻¹' K₀) := by + have := φ.openEmbedding + refine isCompact_of_isClosed_isBounded ?hc ?hb + sorry + replace K₁_cpct : IsCompact (φ ⁻¹' K₁) := sorry + have K₀K₁' : φ ⁻¹' K₀ ⊆ interior (φ ⁻¹' K₁) := sorry + sorry/- simp only [P₀, forall_and] at P₀f + rcases P₀f with ⟨hf_sec, hf_sol, hf_smooth, hf_A, hf_dist⟩ + rw [forall_restrictGermPredicate_iff] at hf_A + let F : FormalSol R := mkFormalSol f hf_sec hf_sol hf_smooth + have hFAC : ∀ᶠ x near A ∪ C, F.IsHolonomicAt x := + by + rw [eventually_nhdsSet_union] + refine' ⟨_, fC⟩ + apply (hf_A.and h𝓕₀).eventually_nhdsSet.mono fun x hx ↦ ?_ + rw [eventually_and] at hx + apply hx.2.self_of_nhds.congr + apply hx.1.mono fun x' hx' ↦ ?_ + simp [F] + exact hx'.symm + have hFφψ : F.bs '' (range φ) ⊆ range ψ := by + rw [← range_comp] + apply hφψ + intro x + calc + dist (F.bs x) (𝓕₀.bs x) = dist (f x).1.2 (𝓕₀.bs x) := by simp only [F, mkFormalSol_bs_apply] + _ < τ x := (hf_dist x) + _ ≤ ε x := min_le_right _ _ + let η : M → ℝ := fun x ↦ τ x - dist (f x).1.2 (𝓕₀.bs x) + have η_pos : ∀ x, 0 < η x := fun x ↦ sub_pos.mpr (hf_dist x) + have η_cont : Continuous η := + by + have : ContMDiff IM ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ f := fun x ↦ hf_smooth x + apply τ_cont.sub + exact (one_jet_bundle_proj_continuous.comp this.continuous).snd.dist 𝓕₀.smooth_bs.continuous + rcases φ.improve_formalSol ψ hRample hRopen (hA.union C_closed) η_pos η_cont hFφψ hFAC K₀_cpct + K₁_cpct K₀K₁' with + ⟨F', hF'₀, hF'₁, hF'AC, hF'K₁, hF'η, hF'hol⟩ + refine' ⟨fun t x ↦ F' t x, _, _, _, _, _, _⟩ ; all_goals beta_reduce + · refine' fun t x ↦ ⟨rfl, F'.is_sol, (F' t).smooth x, _, _⟩ + · revert x + rw [forall_restrictGermPredicate_iff] + rw [eventually_nhdsSet_union] at hF'AC + apply (hF'AC.1.and hf_A).mono + rintro x ⟨hx, hx'⟩ + change F' t x = _ + rw [hx t, ← hx', mkFormalSol_apply] + rfl + · calc + dist (F' t x).1.2 (𝓕₀.bs x) ≤ dist (F' t x).1.2 (F.bs x) + dist (F.bs x) (𝓕₀.bs x) := + dist_triangle _ _ _ + _ < η x + dist (F.bs x) (𝓕₀.bs x) := (add_lt_add_right (hF'η t x) _) + _ = τ x := by simp [η] + · have : K₀ ⊆ range φ := K₀K₁.trans interior_subset |>.trans <| SurjOn.subset_range hK₁ + rw [union_assoc, eventually_nhdsSet_union, image_preimage_eq_of_subset this] at hF'hol + exact hF'hol.2 + · exact F'.smooth + · intro t x hx + replace hx : x ∉ φ '' (φ ⁻¹' K₁) := by + rwa [image_preimage_eq_of_subset (SurjOn.subset_range hK₁)] + simpa using hF'K₁ t x hx + · apply hF'₀.mono fun x hx ↦ ?_ + erw [hx] + ext1 y + simp [F] + · apply hF'₁.mono fun x hx ↦ ?_ + rw [hx] -/ + +/- rcases inductive_htpy_construction' P₀ P₁ P₂ hP₂ hP₂' init ind with ⟨F, hF₀, hFP₀, hFP₁, hFP₂⟩ +simp only [P₀, forall₂_and_distrib] at hFP₀ +rcases hFP₀ with ⟨hF_sec, hF_sol, _hF_smooth, hF_A, hF_dist⟩ +refine' ⟨mkHtpyFormalSol F hF_sec hF_sol hFP₂, _, _, _, _⟩ +· intro x + rw [mkHtpyFormalSol_apply, hF₀] +· exact hFP₁ +· intro x hx t + rw [mkHtpyFormalSol_apply] + exact (forall_restrictGermPredicate_iff.mp <| hF_A t).on_set x hx +· intro t x + change dist (mkHtpyFormalSol F hF_sec hF_sol hFP₂ t x).1.2 (𝓕₀.bs x) ≤ δ x + rw [mkHtpyFormalSol_apply] + exact (hF_dist t x).le.trans (min_le_left _ _) -/ + theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R) (hA : IsClosed A) (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) : R.SatisfiesHPrinciple A δ := by borelize EX @@ -57,43 +266,43 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R -- We now start the main proof under the assumption that `M` and `X` are nonempty. have cont : Continuous 𝓕₀.bs := 𝓕₀.smooth_bs.continuous let L : LocalisationData IM IX 𝓕₀.bs := stdLocalisationData EM IM EX IX cont - let K : IndexType L.N → Set M := fun i => L.φ i '' closedBall (0 : EM) 1 - let U : IndexType L.N → Set M := fun i => range (L.φ i) + let K : IndexType L.N → Set M := fun i ↦ L.φ i '' closedBall (0 : EM) 1 + let U : IndexType L.N → Set M := fun i ↦ range (L.φ i) have K_cover : (⋃ i, K i) = univ := - eq_univ_of_subset (iUnion_mono fun i => image_subset _ ball_subset_closedBall) L.h₁ - let τ := fun x : M => min (δ x) (L.ε x) - have τ_pos : ∀ x, 0 < τ x := fun x => lt_min (hδ_pos x) (L.ε_pos x) + eq_univ_of_subset (iUnion_mono fun i ↦ image_subset _ ball_subset_closedBall) L.h₁ + let τ := fun x : M ↦ min (δ x) (L.ε x) + have τ_pos : ∀ x, 0 < τ x := fun x ↦ lt_min (hδ_pos x) (L.ε_pos x) have τ_cont : Continuous τ := hδ_cont.min L.ε_cont - have := fun (x : M) (F' : Germ (𝓝 x) J¹) => F'.value = 𝓕₀ x - let P₀ : ∀ x : M, Germ (𝓝 x) J¹ → Prop := fun x F => + have := fun (x : M) (F' : Germ (𝓝 x) J¹) ↦ F'.value = 𝓕₀ x + let P₀ : ∀ x : M, Germ (𝓝 x) J¹ → Prop := fun x F ↦ F.value.1.1 = x ∧ F.value ∈ R ∧ F.ContMDiffAt' IM ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ ∧ - RestrictGermPredicate (fun x F' => F'.value = 𝓕₀ x) A x F ∧ + RestrictGermPredicate (fun x F' ↦ F'.value = 𝓕₀ x) A x F ∧ dist F.value.1.2 (𝓕₀.bs x) < τ x - let P₁ : ∀ x : M, Germ (𝓝 x) J¹ → Prop := fun x F => IsHolonomicGerm F - let P₂ : ∀ p : ℝ × M, Germ (𝓝 p) J¹ → Prop := fun p F => + let P₁ : ∀ x : M, Germ (𝓝 x) J¹ → Prop := fun x F ↦ IsHolonomicGerm F + let P₂ : ∀ p : ℝ × M, Germ (𝓝 p) J¹ → Prop := fun p F ↦ F.ContMDiffAt' (𝓘(ℝ).prod IM) ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ have hP₂ : ∀ (a b : ℝ) (p : ℝ × M) (f : ℝ × M → OneJetBundle IM M IX X), - P₂ (a * p.1 + b, p.2) f → P₂ p fun p : ℝ × M => f (a * p.1 + b, p.2) := + P₂ (a * p.1 + b, p.2) f → P₂ p fun p : ℝ × M ↦ f (a * p.1 + b, p.2) := by rintro a b ⟨t, x⟩ f h - change ContMDiffAt _ _ _ (f ∘ fun p : ℝ × M => (a * p.1 + b, p.2)) (t, x) - change ContMDiffAt _ _ _ f ((fun p : ℝ × M => (a * p.1 + b, p.2)) (t, x)) at h + change ContMDiffAt _ _ _ (f ∘ fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x) + change ContMDiffAt _ _ _ f ((fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x)) at h have : - ContMDiffAt (𝓘(ℝ, ℝ).prod IM) (𝓘(ℝ, ℝ).prod IM) ∞ (fun p : ℝ × M => (a * p.1 + b, p.2)) + ContMDiffAt (𝓘(ℝ, ℝ).prod IM) (𝓘(ℝ, ℝ).prod IM) ∞ (fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x) := - haveI h₁ : ContMDiffAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ∞ (fun t => a * t + b) t := + haveI h₁ : ContMDiffAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ∞ (fun t ↦ a * t + b) t := contMDiffAt_iff_contDiffAt.mpr (((contDiffAt_id : ContDiffAt ℝ ∞ id t).const_smul a).add contDiffAt_const) h₁.prod_map contMDiffAt_id exact h.comp (t, x) this have init : ∀ x : M, P₀ x (𝓕₀ : M → J¹) := by - refine' fun x => ⟨rfl, 𝓕₀.is_sol x, 𝓕₀.smooth x, _, _⟩ + refine' fun x ↦ ⟨rfl, 𝓕₀.is_sol x, 𝓕₀.smooth x, _, _⟩ · revert x - exact forall_restrictGermPredicate_of_forall fun x => rfl + exact forall_restrictGermPredicate_of_forall fun x ↦ rfl · erw [dist_self] exact τ_pos x have ind : @@ -119,7 +328,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R let C := ⋃ j < i, L.φ j '' closedBall 0 1 have hC : IsClosed C :=-- TODO: rewrite localization_data.is_closed_Union to match this. - (finite_Iio _).isClosed_biUnion fun j _hj => (hK₀.image <| (L.φ j).continuous).isClosed + (finite_Iio _).isClosed_biUnion fun j _hj ↦ (hK₀.image <| (L.φ j).continuous).isClosed simp only [P₀, forall_and] at hf₀ rcases hf₀ with ⟨hf_sec, hf_sol, hf_smooth, hf_A, hf_dist⟩ rw [forall_restrictGermPredicate_iff] at hf_A @@ -128,10 +337,10 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R by rw [eventually_nhdsSet_union] refine' ⟨_, hf₁⟩ - apply (hf_A.and h𝓕₀).eventually_nhdsSet.mono fun x hx => ?_ + apply (hf_A.and h𝓕₀).eventually_nhdsSet.mono fun x hx ↦ ?_ rw [eventually_and] at hx apply hx.2.self_of_nhds.congr - apply hx.1.mono fun x' hx' => ?_ + apply hx.1.mono fun x' hx' ↦ ?_ simp [F] exact hx'.symm have hFφψ : F.bs '' (range <| L.φ i) ⊆ range (L.ψj i) := @@ -143,18 +352,18 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R dist (F.bs x) (𝓕₀.bs x) = dist (f x).1.2 (𝓕₀.bs x) := by simp only [F, mkFormalSol_bs_apply] _ < τ x := (hf_dist x) _ ≤ L.ε x := min_le_right _ _ - let η : M → ℝ := fun x => τ x - dist (f x).1.2 (𝓕₀.bs x) - have η_pos : ∀ x, 0 < η x := fun x => sub_pos.mpr (hf_dist x) + let η : M → ℝ := fun x ↦ τ x - dist (f x).1.2 (𝓕₀.bs x) + have η_pos : ∀ x, 0 < η x := fun x ↦ sub_pos.mpr (hf_dist x) have η_cont : Continuous η := by - have : ContMDiff IM ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ f := fun x => hf_smooth x + have : ContMDiff IM ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ f := fun x ↦ hf_smooth x apply τ_cont.sub exact (one_jet_bundle_proj_continuous.comp this.continuous).snd.dist 𝓕₀.smooth_bs.continuous rcases(L.φ i).improve_formalSol (L.ψj i) hRample hRopen (hA.union hC) η_pos η_cont hFφψ hFAC hK₀ hK₁ hK₀K₁ with ⟨F', hF'₀, hF'₁, hF'AC, hF'K₁, hF'η, hF'hol⟩ - refine' ⟨fun t x => F' t x, _, _, _, _, _, _⟩ ; all_goals beta_reduce - · refine' fun t x => ⟨rfl, F'.is_sol, (F' t).smooth x, _, _⟩ + refine' ⟨fun t x ↦ F' t x, _, _, _, _, _, _⟩ ; all_goals beta_reduce + · refine' fun t x ↦ ⟨rfl, F'.is_sol, (F' t).smooth x, _, _⟩ · revert x rw [forall_restrictGermPredicate_iff] rw [eventually_nhdsSet_union] at hF'AC @@ -177,11 +386,11 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R · intro t x hx rw [hF'K₁ t x ((mem_range_of_mem_image _ _).mt hx)] simp [F] - · apply hF'₀.mono fun x hx => ?_ + · apply hF'₀.mono fun x hx ↦ ?_ erw [hx] ext1 y simp [F] - · apply hF'₁.mono fun x hx => ?_ + · apply hF'₁.mono fun x hx ↦ ?_ rw [hx] rcases inductive_htpy_construction P₀ P₁ P₂ hP₂ L.lf_φ K_cover init (𝓕₀.smooth.comp contMDiff_snd) ind with @@ -214,10 +423,9 @@ which ensures the ampleness assumption survives this reduction. /-- **Gromov's Theorem** -/ theorem RelMfld.Ample.satisfiesHPrincipleWith (hRample : R.Ample) (hRopen : IsOpen R) (hC : IsClosed C) (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) : - R.SatisfiesHPrincipleWith IP C δ := - by - have hδ_pos' : ∀ x : P × M, 0 < δ x.2 := fun x : P × M => hδ_pos x.snd - have hδ_cont' : Continuous fun x : P × M => δ x.2 := hδ_cont.comp continuous_snd + R.SatisfiesHPrincipleWith IP C δ := by + have hδ_pos' : ∀ x : P × M, 0 < δ x.2 := fun x : P × M ↦ hδ_pos x.snd + have hδ_cont' : Continuous fun x : P × M ↦ δ x.2 := hδ_cont.comp continuous_snd have is_op : IsOpen (RelMfld.relativize IP P R) := R.isOpen_relativize hRopen apply RelMfld.SatisfiesHPrinciple.satisfiesHPrincipleWith exact (hRample.relativize IP P).satisfiesHPrinciple is_op hC hδ_pos' hδ_cont' diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean index 67a55fc6..debaf739 100644 --- a/SphereEversion/Global/LocalisationData.lean +++ b/SphereEversion/Global/LocalisationData.lean @@ -155,8 +155,10 @@ theorem ε_spec (ld : LocalisationData I I' f) : range (g ∘ ld.φ i) ⊆ range (ld.ψj i) := (localisation_stability ld).choose_spec.choose_spec.choose_spec -theorem exists_stability_dist {f : M → M'} (hf : Continuous f) : - ∃ ε > (0 : M → ℝ), Continuous ε ∧ +variable (I I') + +theorem _root_.exists_stability_dist {f : M → M'} (hf : Continuous f) : + ∃ ε : M → ℝ, (∀ m, 0 < ε m) ∧ Continuous ε ∧ ∀ x : M, ∃ φ : OpenSmoothEmbedding 𝓘(ℝ, E) E I M, ∃ ψ : OpenSmoothEmbedding 𝓘(ℝ, E') E' I' M',