From 57a652c2cfc87031a7e6dc4fb87366c4a0bcd211 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Wed, 6 Dec 2023 14:23:23 -0500 Subject: [PATCH] Variant --- SphereEversion/InductiveConstructions.lean | 44 +++++++++++++++------- 1 file changed, 31 insertions(+), 13 deletions(-) diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index cb49ce13..1832d7c7 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -98,20 +98,12 @@ theorem inductive_construction {X Y : Type _} [TopologicalSpace X] {N : ℕ} {U rcases((hF x).and <| eventually_ge_atTop j).exists with ⟨n₀, hn₀, hn₀'⟩ exact Eventually.germ_congr (h₁f _ _ hn₀' x) hn₀.symm -/-- We are given a suitably nice extended metric space `X` and three local constraints `P₀`,`P₀'` -and `P₁` on maps from `X` to some type `Y`. All maps entering the discussion are required to -statisfy `P₀` everywhere. The goal is to turn a map `f₀` satisfying `P₁` near a compact set `K` into -one satisfying everywhere without changing `f₀` near `K`. The assumptions are: -* For every `x` in `X` there is a map which satisfies `P₁` near `x` -* One can patch two maps `f₁ f₂` satisfying `P₁` on open sets `U₁` and `U₂` respectively - and such that `f₁` satisfies `P₀'` everywhere into a map satisfying `P₁` on `K₁ ∪ K₂` for any - compact sets `Kᵢ ⊆ Uᵢ` and `P₀'` everywhere. -/ -theorem inductive_construction_of_loc {X Y : Type _} [EMetricSpace X] [LocallyCompactSpace X] +theorem inductive_construction_of_loc' {X Y : Type _} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] (P₀ P₀' P₁ : ∀ x : X, Germ (𝓝 x) Y → Prop) {f₀ : X → Y} (hP₀f₀ : ∀ x, P₀ x f₀ ∧ P₀' x f₀) (loc : ∀ x, ∃ f : X → Y, (∀ x, P₀ x f) ∧ ∀ᶠ x' in 𝓝 x, P₁ x' f) (ind : ∀ {U₁ U₂ K₁ K₂ : Set X} {f₁ f₂ : X → Y}, IsOpen U₁ → IsOpen U₂ → - IsClosed K₁ → IsClosed K₂ → K₁ ⊆ U₁ → K₂ ⊆ U₂ → + IsCompact K₁ → IsCompact K₂ → K₁ ⊆ U₁ → K₂ ⊆ U₂ → (∀ x, P₀ x f₁ ∧ P₀' x f₁) → (∀ x, P₀ x f₂) → (∀ x ∈ U₁, P₁ x f₁) → (∀ x ∈ U₂, P₁ x f₂) → ∃ f : X → Y, (∀ x, P₀ x f ∧ P₀' x f) ∧ (∀ᶠ x near K₁ ∪ K₂, P₁ x f) ∧ ∀ᶠ x near K₁ ∪ U₂ᶜ, f x = f₁ x) : @@ -132,11 +124,11 @@ theorem inductive_construction_of_loc {X Y : Type _} [EMetricSpace X] [LocallyCo (∀ j ≤ i, ∀ x, RestrictGermPredicate P₁ (K j) x f') ∧ ∀ x, x ∉ U i → f' x = f x := by simp_rw [forall_restrictGermPredicate_iff, ← eventually_nhdsSet_iUnion₂] rintro (i : ℕ) f h₀f h₁f - have cpct : IsClosed (⋃ j < i, K j) := - (finite_lt_nat i).isClosed_biUnion fun j _ => (K_cpct j).isClosed + have cpct : IsCompact (⋃ j < i, K j) := + (finite_lt_nat i).isCompact_biUnion fun j _ ↦ K_cpct j rcases hU i with ⟨f', h₀f', h₁f'⟩ rcases mem_nhdsSet_iff_exists.mp h₁f with ⟨V, V_op, hKV, h₁V⟩ - rcases ind V_op (U_op i) cpct (K_cpct i).isClosed hKV (hKU i) h₀f h₀f' h₁V h₁f' with + rcases ind V_op (U_op i) cpct (K_cpct i) hKV (hKU i) h₀f h₀f' h₁V h₁f' with ⟨F, h₀F, h₁F, hF⟩ simp_rw [← bUnion_le] at h₁F exact ⟨F, h₀F, h₁F, fun x hx => hF.on_set x (Or.inr hx)⟩ @@ -149,6 +141,32 @@ theorem inductive_construction_of_loc {X Y : Type _} [EMetricSpace X] [LocallyCo rcases mem_iUnion.mp (hK trivial : x ∈ ⋃ j, K j) with ⟨j, hj⟩ exact (h' j x hj).self_of_nhds + +/-- We are given a suitably nice extended metric space `X` and three local constraints `P₀`,`P₀'` +and `P₁` on maps from `X` to some type `Y`. All maps entering the discussion are required to +statisfy `P₀` everywhere. The goal is to turn a map `f₀` satisfying `P₁` near a compact set `K` into +one satisfying everywhere without changing `f₀` near `K`. The assumptions are: +* For every `x` in `X` there is a map which satisfies `P₁` near `x` +* One can patch two maps `f₁ f₂` satisfying `P₁` on open sets `U₁` and `U₂` respectively + and such that `f₁` satisfies `P₀'` everywhere into a map satisfying `P₁` on `K₁ ∪ K₂` for any + compact sets `Kᵢ ⊆ Uᵢ` and `P₀'` everywhere. -/ +theorem inductive_construction_of_loc {X Y : Type _} [EMetricSpace X] [LocallyCompactSpace X] + [SecondCountableTopology X] (P₀ P₀' P₁ : ∀ x : X, Germ (𝓝 x) Y → Prop) {f₀ : X → Y} + (hP₀f₀ : ∀ x, P₀ x f₀ ∧ P₀' x f₀) + (loc : ∀ x, ∃ f : X → Y, (∀ x, P₀ x f) ∧ ∀ᶠ x' in 𝓝 x, P₁ x' f) + (ind : ∀ {U₁ U₂ K₁ K₂ : Set X} {f₁ f₂ : X → Y}, IsOpen U₁ → IsOpen U₂ → + IsClosed K₁ → IsClosed K₂ → K₁ ⊆ U₁ → K₂ ⊆ U₂ → + (∀ x, P₀ x f₁ ∧ P₀' x f₁) → (∀ x, P₀ x f₂) → (∀ x ∈ U₁, P₁ x f₁) → (∀ x ∈ U₂, P₁ x f₂) → + ∃ f : X → Y, (∀ x, P₀ x f ∧ P₀' x f) ∧ + (∀ᶠ x near K₁ ∪ K₂, P₁ x f) ∧ ∀ᶠ x near K₁ ∪ U₂ᶜ, f x = f₁ x) : + ∃ f : X → Y, ∀ x, P₀ x f ∧ P₀' x f ∧ P₁ x f := by + apply inductive_construction_of_loc' P₀ P₀' P₁ hP₀f₀ loc + intro U₁ U₂ K₁ K₂ f₁ f₂ hU₁ hU₂ hK₁ hK₂ + replace hK₁ := hK₁.isClosed + replace hK₂ := hK₂.isClosed + solve_by_elim + + /-- We are given a suitably nice extended metric space `X` and three local constraints `P₀`,`P₀'` and `P₁` on maps from `X` to some type `Y`. All maps entering the discussion are required to statisfy `P₀` everywhere. The goal is to turn a map `f₀` satisfying `P₁` near a compact set `K` into