diff --git a/SphereEversion.lean b/SphereEversion.lean index fbb06ae8..b4d98b31 100644 --- a/SphereEversion.lean +++ b/SphereEversion.lean @@ -12,7 +12,6 @@ import SphereEversion.Global.TwistOneJetSec import SphereEversion.Indexing import SphereEversion.InductiveConstructions import SphereEversion.Local.AmpleRelation -import SphereEversion.Local.AmpleSet import SphereEversion.Local.Corrugation import SphereEversion.Local.DualPair import SphereEversion.Local.HPrinciple @@ -27,6 +26,7 @@ import SphereEversion.Loops.Reparametrization import SphereEversion.Loops.Surrounding import SphereEversion.Main import SphereEversion.Notations +import SphereEversion.ToMathlib.Algebra.Periodic import SphereEversion.ToMathlib.Analysis.Calculus import SphereEversion.ToMathlib.Analysis.Calculus.AffineMap import SphereEversion.ToMathlib.Analysis.ContDiff @@ -65,5 +65,4 @@ import SphereEversion.ToMathlib.Topology.HausdorffDistance import SphereEversion.ToMathlib.Topology.Misc import SphereEversion.ToMathlib.Topology.Paracompact import SphereEversion.ToMathlib.Topology.Path -import SphereEversion.ToMathlib.Topology.Periodic import SphereEversion.ToMathlib.Topology.Separation diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 4197904a..3ed69c43 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -1,8 +1,8 @@ +import Mathlib.Analysis.Convex.AmpleSet import Mathlib.Geometry.Manifold.Instances.Sphere import SphereEversion.ToMathlib.LinearAlgebra.FiniteDimensional import SphereEversion.ToMathlib.Geometry.Manifold.Immersion import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation -import SphereEversion.Local.AmpleSet import SphereEversion.Global.Gromov import SphereEversion.Global.TwistOneJetSec diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index 539ba489..bf795de0 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -1,6 +1,5 @@ import SphereEversion.Global.Relation import Mathlib.Analysis.Convex.AmpleSet -import SphereEversion.Local.AmpleSet noncomputable section diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index e54669a7..c3c9d1b9 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -146,7 +146,7 @@ theorem forall_near [T2Space M'] {P : M → Prop} {P' : M' → Prop} {K : Set M} rw [show A = A ∩ range f ∪ A ∩ (range f)ᶜ by simp] apply Filter.Eventually.union · have : ∀ᶠ m' near A ∩ range f, m' ∈ range f := - f.isOpen_range.mem_nhdsSet.mpr (inter_subset_right _ _) + f.isOpen_range.mem_nhdsSet.mpr inter_subset_right apply (this.and <| f.forall_near' hP).mono rintro _ ⟨⟨m, rfl⟩, hm⟩ exact hPP' _ (hm _ rfl) diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean index 6357b1b7..dc44dfe7 100644 --- a/SphereEversion/Indexing.lean +++ b/SphereEversion/Indexing.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.Fin.Interval +import Mathlib.Order.Interval.Finset.Fin import Mathlib.Data.Fin.SuccPred import Mathlib.Data.Nat.SuccPred import Mathlib.Data.ZMod.Defs diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 57e85bf6..7ffcddba 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -174,29 +174,26 @@ theorem set_juggling {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X · exact IsOpen.union U₁_op U_op · exact IsOpen.sdiff U₂_op hK · refine IsCompact.union K₁_cpct ?_ - refine K₂_cpct.closure_of_subset ?_ - exact inter_subset_left K₂ U' + exact K₂_cpct.closure_of_subset inter_subset_left · exact IsCompact.diff K₂_cpct U'_op - · exact subset_union_left K₁ (closure (K₂ ∩ U')) + · exact subset_union_left · apply union_subset_union exact hK₁U₁ apply subset_trans _ hU'U gcongr - exact inter_subset_right K₂ U' + exact inter_subset_right · exact diff_subset_diff hK₂U₂ hKU' · rw [union_assoc] congr apply subset_antisymm - · apply union_subset - · apply K₂_cpct.isClosed.closure_subset_iff.mpr - exact inter_subset_left K₂ U' - · exact diff_subset K₂ U' + · apply union_subset ?_ diff_subset + exact K₂_cpct.isClosed.closure_subset_iff.mpr inter_subset_left · calc K₂ = K₂ ∩ U' ∪ K₂ \ U' := (inter_union_diff K₂ U').symm _ ⊆ closure (K₂ ∩ U') ∪ K₂ \ U' := union_subset_union_left (K₂ \ U') subset_closure · intro x hx hx' exact hx'.2 hx · rw [union_comm] - · exact diff_subset U₂ K + · exact diff_subset /-- 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 diff --git a/SphereEversion/Local/AmpleRelation.lean b/SphereEversion/Local/AmpleRelation.lean index 5e069613..065fd8bf 100644 --- a/SphereEversion/Local/AmpleRelation.lean +++ b/SphereEversion/Local/AmpleRelation.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Patrick Massot. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Patrick Massot -/ -import SphereEversion.Local.AmpleSet +import Mathlib.Analysis.Convex.AmpleSet import SphereEversion.Local.DualPair import SphereEversion.Local.Relation diff --git a/SphereEversion/Local/AmpleSet.lean b/SphereEversion/Local/AmpleSet.lean deleted file mode 100644 index 59ee4c36..00000000 --- a/SphereEversion/Local/AmpleSet.lean +++ /dev/null @@ -1,53 +0,0 @@ -/- -Copyright (c) 2021 Anatole Dedecker. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Anatole Dedecker, Floris van Doorn --/ -import Mathlib.Analysis.Convex.AmpleSet -import Mathlib.Analysis.NormedSpace.Connected - -/-! -# Ample subsets of real vector spaces - -In this file we study ample set in real vector spaces. A set is ample if all its connected -component have full convex hull. We then prove this property is invariant under a number of affine -geometric operations. - -As trivial examples, the empty set and the univ set are ample. After proving those fact, -the second part of the file proves that a linear subspace with codimension at least 2 has a -ample complement. This is the crucial geometric ingredient which allows to apply convex integration -to the theory of immersions in positive codimension. - -All vector spaces in the file (and more generally in this folder) are real vector spaces. - -## Implementation notes - -The definition of ample subset asks for a vector space structure and a topology on the ambient type -without any link between those structures, but we will only be using these for finite dimensional -vector spaces with their natural topology. --/ - -/-! ## Subspaces of codimension at least 2 have ample complement -/ -section Lemma213 - -open Set -variable {F : Type*} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] - [TopologicalAddGroup F] [ContinuousSMul ℝ F] - --- PRed in #11342 -/-- Let `E` be a linear subspace in a real vector space. If `E` has codimension at -least two then its complement is ample. -/ -theorem AmpleSet.of_one_lt_codim {E : Submodule ℝ F} (hcodim : 1 < Module.rank ℝ (F ⧸ E)) : - AmpleSet (Eᶜ : Set F) := fun x hx ↦ by - rw [E.connectedComponentIn_eq_self_of_one_lt_codim hcodim hx, eq_univ_iff_forall] - intro y - by_cases h : y ∈ E - · obtain ⟨z, hz⟩ : ∃ z, z ∉ E := by - rw [← not_forall, ← Submodule.eq_top_iff'] - rintro rfl - simp [rank_zero_iff.2 inferInstance] at hcodim - refine segment_subset_convexHull ?_ ?_ (mem_segment_sub_add y z) <;> - simpa [sub_eq_add_neg, Submodule.add_mem_iff_right _ h] - · exact subset_convexHull ℝ (Eᶜ : Set F) h - -end Lemma213 diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean index 4e222944..be880d0e 100644 --- a/SphereEversion/Local/Corrugation.lean +++ b/SphereEversion/Local/Corrugation.lean @@ -2,7 +2,7 @@ import Mathlib.Analysis.Asymptotics.Asymptotics import Mathlib.LinearAlgebra.Dual import Mathlib.MeasureTheory.Integral.Periodic import Mathlib.Analysis.Calculus.ParametricIntegral -import SphereEversion.ToMathlib.Topology.Periodic +import SphereEversion.ToMathlib.Algebra.Periodic import SphereEversion.ToMathlib.MeasureTheory.BorelSpace import SphereEversion.Loops.Basic import SphereEversion.Local.DualPair diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index 784a8ccf..1941b813 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -154,7 +154,7 @@ theorem smooth_g (L : StepLandscape E) (𝓕 : JetSec E F) : 𝒞 ∞ (L.g 𝓕) theorem Accepts.rel {L : StepLandscape E} {𝓕 : JetSec E F} (h : L.Accepts R 𝓕) : ∀ᶠ x : E near L.K, (L.g 𝓕) x = (L.b 𝓕) x := by - apply (h.hC.filter_mono <| monotone_nhdsSet (inter_subset_right L.K₁ L.C)).mono + apply (h.hC.filter_mono <| monotone_nhdsSet inter_subset_right).mono intro x hx dsimp [JetSec.IsHolonomicAt] at hx dsimp [StepLandscape.g, StepLandscape.b] diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index 9793254f..d333e6aa 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -1,7 +1,7 @@ +import Mathlib.Analysis.Convex.AmpleSet import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual import SphereEversion.Local.ParametricHPrinciple -import SphereEversion.Local.AmpleSet /-! This is file proves the existence of a sphere eversion from the local verson of the h-principle. diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean index 26e765b6..1eee4e93 100644 --- a/SphereEversion/Loops/DeltaMollifier.lean +++ b/SphereEversion/Loops/DeltaMollifier.lean @@ -3,7 +3,7 @@ import Mathlib.MeasureTheory.Integral.Periodic import Mathlib.Analysis.Convolution import Mathlib.MeasureTheory.Measure.Haar.Unique import Mathlib.Analysis.Calculus.BumpFunction.Normed -import SphereEversion.ToMathlib.Topology.Periodic +import SphereEversion.ToMathlib.Algebra.Periodic import SphereEversion.ToMathlib.Analysis.ContDiff import SphereEversion.Loops.Basic @@ -189,7 +189,7 @@ theorem intervalIntegral_periodize_smul (f : ℝ → ℝ) (γ : Loop E) {a b c d rw [h2] have : (support fun t ↦ f t • γ t) ⊆ Ioc a (a + 1) := by erw [support_smul] - exact ((inter_subset_left _ _).trans hf).trans (Ioc_subset_Ioc_right h) + exact (inter_subset_left.trans hf).trans (Ioc_subset_Ioc_right h) rw [← intervalIntegral.integral_eq_integral_of_support_subset this] simp_rw [periodize_smul_periodic _ γ.periodic, Function.Periodic.intervalIntegral_add_eq (periodic_periodize fun x : ℝ ↦ f x • γ x) c a] diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 56ceb19a..c6ed42d6 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -147,8 +147,8 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : have h2C₁ : ∀ (s : ℝ) (hs : fract s = 0), fract ⁻¹' C₁ ∈ 𝓝 s := by intro s hs refine fract_preimage_mem_nhds ?_ fun _ ↦ ?_ - · rw [hs]; exact mem_of_superset (Iic_mem_nhds <| by norm_num) (subset_union_left _ _) - · exact mem_of_superset (Ici_mem_nhds <| by norm_num) (subset_union_right _ _) + · rw [hs]; exact mem_of_superset (Iic_mem_nhds <| by norm_num) subset_union_left + · exact mem_of_superset (Ici_mem_nhds <| by norm_num) subset_union_right let C : Set (E × ℝ × ℝ) := (fun x ↦ x.2.1) ⁻¹' Iic (5⁻¹ : ℝ) ∪ (fun x ↦ fract x.2.2) ⁻¹' C₁ have hC : IsClosed C := by refine (isClosed_Iic.preimage continuous_snd.fst).union ?_ @@ -191,7 +191,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : have : (fun x : E × ℝ × ℝ ↦ (x.1, smoothTransition x.2.1, fract x.2.2)) ⁻¹' C ∈ 𝓝 (x, t, s) := by simp_rw [C, preimage_union, preimage_preimage, fract_fract] - refine mem_of_superset ?_ (subset_union_right _ _) + refine mem_of_superset ?_ subset_union_right refine continuousAt_id.snd'.snd'.preimage_mem_nhds (h2C₁ s hs) filter_upwards [this] with x hx exact (hγ₅C hx).trans diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index bb3f230d..9070b3d6 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -218,16 +218,15 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w : have hA : IsOpen A := by simp only [A, affineBases_findim ι ℝ F hι] exact isOpen_univ.prod (isOpen_affineIndependent ℝ F) - have hU₁ : U ⊆ A := Set.inter_subset_left _ _ have hU₂ : IsOpen U := hW'.isOpen_inter_preimage hA hV have hU₃ : U ∈ 𝓝 (x, p) := mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, Set.mem_inter (by simp [hp, A]) (mem_preimage.mpr hxp)⟩ apply eventually_of_mem hU₃ rintro ⟨y, q⟩ hyq - have hq : q ∈ affineBases ι ℝ F := by simpa [A] using hU₁ hyq - have hyq' : (y, q) ∈ W' ⁻¹' V := (Set.inter_subset_right _ _) hyq - refine ⟨⟨U, mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, hyq⟩, (smooth_barycentric ι ℝ F hι).mono hU₁⟩, - ?_, ?_, ?_⟩ + have hq : q ∈ affineBases ι ℝ F := by simpa [A] using inter_subset_left hyq + have hyq' : (y, q) ∈ W' ⁻¹' V := inter_subset_right hyq + refine ⟨⟨U, mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, hyq⟩, + (smooth_barycentric ι ℝ F hι).mono inter_subset_left⟩, ?_, ?_, ?_⟩ · simpa [V] using hyq' · simp [hq] · simp [hq]; exact AffineBasis.linear_combination_coord_eq_self _ y @@ -671,7 +670,7 @@ theorem local_loops [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈ rw [hδx₀] show Ω ∈ 𝓝 (x₀, γ t s) exact mem_nhds_iff.mpr - ⟨_, inter_subset_left _ _, hU, ⟨h5γ t s, show x₀ ∈ U from mem_of_mem_nhds hUx₀⟩⟩ + ⟨_, inter_subset_left, hU, ⟨h5γ t s, show x₀ ∈ U from mem_of_mem_nhds hUx₀⟩⟩ refine this.mono ?_; intro x h t ht s hs; exact h (t, s) ⟨ht, hs⟩ have hδsurr : ∀ᶠ x in 𝓝 x₀, (δ x 1).Surrounds (g x) := by rcases h6γ with ⟨p, w, h⟩ @@ -866,7 +865,7 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ have hV₀L₁ : Disjoint (closure V₀) L₁ := disjoint_sdiff_self_right.mono hVU₀ Subset.rfl obtain ⟨V₂, hV₂, hLV₂, h2V₂⟩ := normal_exists_closure_subset hL₁ (isClosed_closure.isOpen_compl.inter hU₁) - (subset_inter (subset_compl_iff_disjoint_left.mpr hV₀L₁) <| (diff_subset _ _).trans hKU₁) + (subset_inter (subset_compl_iff_disjoint_left.mpr hV₀L₁) <| diff_subset.trans hKU₁) obtain ⟨V₁, hV₁, hLV₁, hV₁₂⟩ := normal_exists_closure_subset hL₁ hV₂ hLV₂ rw [subset_inter_iff, subset_compl_iff_disjoint_left] at h2V₂ rcases h2V₂ with ⟨hV₀₂, hV₂U₁⟩ @@ -875,21 +874,21 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ refine Disjoint.union_left (hV₀₂.mono_right (hV₁₂.trans subset_closure)) ?_ rw [← subset_compl_iff_disjoint_left, compl_compl]; exact hV₁₂ refine ⟨V₀ ∪ U₁ ∩ U₀ ∪ V₁, ((hV₀.union <| hU₁.inter hU₀).union hV₁).mem_nhdsSet.mpr ?_, ?_⟩ - · refine union_subset (hKV₀.trans <| (subset_union_left _ _).trans <| subset_union_left _ _) ?_ + · refine union_subset (hKV₀.trans <| subset_union_left.trans <| subset_union_left) ?_ rw [← inter_union_diff K₁]; - exact union_subset_union ((inter_subset_inter_left _ hKU₁).trans <| subset_union_right _ _) hLV₁ + exact union_subset_union ((inter_subset_inter_left _ hKU₁).trans <| subset_union_right) hLV₁ obtain ⟨ρ, h0ρ, h1ρ, -⟩ := exists_continuous_zero_one_of_isClosed (isClosed_closure.union hV₂.isClosed_compl) isClosed_closure hdisj - let h₀' : SurroundingFamilyIn g b γ₀ (U₁ ∩ U₀) Ω := h₀.mono (inter_subset_right _ _) - let h₁' : SurroundingFamilyIn g b γ₁ (U₁ ∩ U₀) Ω := h₁.mono (inter_subset_left _ _) + let h₀' : SurroundingFamilyIn g b γ₀ (U₁ ∩ U₀) Ω := h₀.mono inter_subset_right + let h₁' : SurroundingFamilyIn g b γ₁ (U₁ ∩ U₀) Ω := h₁.mono inter_subset_left let γ := sfHomotopy h₀'.to_sf h₁'.to_sf have hγ : ∀ τ, SurroundingFamilyIn g b (γ τ) (U₁ ∩ U₀) Ω := surroundingFamilyIn_sfHomotopy h₀' h₁' have heq1 : ∀ x ∈ closure V₀ ∪ V₂ᶜ, γ (ρ x) x = γ₀ x := by intro x hx simp_rw [γ, h0ρ hx, Pi.zero_apply, sfHomotopy_zero] have heq2 : ∀ x ∈ V₀, γ (ρ x) x = γ₀ x := fun x hx ↦ - heq1 x (subset_closure.trans (subset_union_left _ _) hx) + heq1 x (subset_closure.trans subset_union_left hx) refine ⟨fun x t ↦ γ (ρ x) x t, ?_, ?_, ?_⟩ · refine ⟨⟨fun x ↦ (hγ <| ρ x).base x, fun x ↦ (hγ <| ρ x).t₀ x, fun x ↦ (hγ <| ρ x).projI x, ?_, ?_⟩, ?_⟩ @@ -905,7 +904,7 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ · exact hx · exact (hρx <| h1ρ <| subset_closure hx).elim · intro x hx t _ht s hρx; refine h₁.val_in ?_; rcases hx with ((hx | ⟨hx, -⟩) | hx) - · exact (hρx <| h0ρ <| subset_closure.trans (subset_union_left _ _) hx).elim + · exact (hρx <| h0ρ <| subset_closure.trans subset_union_left hx).elim · exact hx · exact hVU₁ hx · exact eventually_of_mem (hV₀.mem_nhdsSet.mpr hKV₀) heq2 diff --git a/SphereEversion/ToMathlib/Topology/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Periodic.lean similarity index 96% rename from SphereEversion/ToMathlib/Topology/Periodic.lean rename to SphereEversion/ToMathlib/Algebra/Periodic.lean index a8d8a8d2..2ce7d9a9 100644 --- a/SphereEversion/ToMathlib/Topology/Periodic.lean +++ b/SphereEversion/ToMathlib/Algebra/Periodic.lean @@ -1,6 +1,6 @@ -import Mathlib.Algebra.Periodic -import Mathlib.Analysis.Normed.Group.Basic import SphereEversion.ToMathlib.Topology.Separation +import Mathlib.Analysis.Normed.Order.Lattice +-- TODO: the file this references doesn't exist in mathlib any more; rename this one appropriately! /-! @@ -101,8 +101,7 @@ theorem image_proj𝕊₁_Icc : proj𝕊₁ '' Icc 0 1 = univ := theorem continuous_proj𝕊₁ : Continuous proj𝕊₁ := continuous_quotient_mk' -theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := - QuotientAddGroup.isOpenMap_coe ℤSubℝ +theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := QuotientAddGroup.isOpenMap_coe ℤSubℝ theorem quotientMap_id_proj𝕊₁ {X : Type*} [TopologicalSpace X] : QuotientMap fun p : X × ℝ ↦ (p.1, proj𝕊₁ p.2) := diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean index 9f623a2f..e2d4079f 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean @@ -7,6 +7,7 @@ Authors: Patrick Massot import Mathlib.Algebra.Ring.Subring.Order import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions import Mathlib.Geometry.Manifold.MFDeriv.Basic +import Mathlib.Order.Filter.Ring import Mathlib.Topology.Germ /-! diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index 5bc14b75..5d9c85e8 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -36,17 +36,17 @@ theorem nhds_hasBasis_balls_of_open_cov [I.Boundaryless] (x : M) {ι : Type*} {s obtain ⟨r, hr₀, hr₁⟩ := (Filter.hasBasis_iff.mp (@nhds_basis_ball E _ (extChartAt I x x)) _).mp hm refine ⟨r, ⟨hr₀, hr₁.trans ?_, ⟨j, ?_⟩⟩, ?_⟩ - · exact ((extChartAt I x).mapsTo.mono (inter_subset_right _ _) Subset.rfl).image_subset + · exact ((extChartAt I x).mapsTo.mono inter_subset_right Subset.rfl).image_subset · suffices m ⊆ s j by refine Subset.trans ?_ this convert monotone_image (f := (extChartAt I x).symm) hr₁ - exact (PartialEquiv.symm_image_image_of_subset_source _ (Set.inter_subset_right _ _)).symm - exact (Set.inter_subset_left _ _).trans (Set.inter_subset_left _ _) + exact (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).symm + exact inter_subset_left.trans inter_subset_left · suffices m ⊆ n by refine Subset.trans ?_ this convert monotone_image (f := (extChartAt I x).symm) hr₁ - exact (PartialEquiv.symm_image_image_of_subset_source _ (Set.inter_subset_right _ _)).symm - exact (Set.inter_subset_left _ _).trans (Set.inter_subset_right _ _) + exact (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).symm + exact inter_subset_left.trans inter_subset_right · rintro ⟨r, ⟨hr₀, hr₁, -⟩, hr₂⟩ replace hr₀ : Metric.ball (extChartAt I x x) r ∈ 𝓝 (extChartAt I x x) := ball_mem_nhds _ hr₀ rw [← map_extChartAt_nhds_of_boundaryless, Filter.mem_map] at hr₀ diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean index c551f57d..e94d03e8 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -130,7 +130,7 @@ theorem hasFDerivAt_parametric_primitive_of_lip' (F : H → ℝ → E) (F' : ℝ rw [hasFDerivAt_iff_hasDerivAt, toSpanSingleton_apply, one_smul] exact intervalIntegral.integral_hasDerivAt_right (hF_int_ball x₀ x₀_in ha hsx₀) ⟨Ioo a₀ b₀, Ioo_nhds, hF_meas x₀ x₀_in⟩ hF_cont - have D₃ : HasFDerivAt (fun x ↦ ∫ t in s x₀..s x, F x t - F x₀ t) 0 x₀ := by + have D₃ : HasFDerivAt (𝕜 := ℝ) (fun x ↦ ∫ t in s x₀..s x, F x t - F x₀ t) 0 x₀ := by refine IsBigO.hasFDerivAt (𝕜 := ℝ) ?_ one_lt_two have O₁ : (fun x ↦ ∫ s in s x₀..s x, bound s) =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ := by have : (fun x ↦ s x - s x₀) =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ := s_diff.isBigO_sub.norm_right diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index c4bd9c29..e30177c2 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -68,7 +68,7 @@ section /-! ## The standard ℤ action on ℝ is properly discontinuous -TODO: use that in ToMathlib.Topology.Periodic? +TODO: use that in ToMathlib.Algebra.Periodic? -/ instance : VAdd ℤ ℝ := @@ -195,7 +195,7 @@ theorem fract_preimage_mem_nhds {s : Set ℝ} {x : ℝ} (h1 : s ∈ 𝓝 (fract obtain ⟨v, hvs, hv, h1v⟩ := mem_nhds_iff.mp (h2 hx) rw [mem_nhds_iff] exact ⟨fract ⁻¹' (u ∪ v), preimage_mono (union_subset hus hvs), - (hu.union hv).preimage_fract fun _ ↦ subset_union_right _ _ h1v, subset_union_left _ _ hxu⟩ + (hu.union hv).preimage_fract fun _ ↦ subset_union_right h1v, subset_union_left hxu⟩ · exact (continuousAt_fract (sub_ne_zero.1 hx)).preimage_mem_nhds h1 end Fract diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean index e91d8e00..5e4d2368 100644 --- a/SphereEversion/ToMathlib/Topology/Paracompact.lean +++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean @@ -1,6 +1,6 @@ import Mathlib.Topology.Separation import Mathlib.Data.Real.Basic -import Mathlib.Data.Nat.Interval +import Mathlib.Order.Interval.Finset.Nat open scoped Topology diff --git a/lake-manifest.json b/lake-manifest.json index 2c11786c..ce2e89d1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,10 +1,10 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06", + "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236", + "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", + "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.36", + "inputRev": "v0.0.38", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb", + "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,10 +58,10 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "7f5ae31cc05ae70ca6c5caaf59985035f040a74e", + "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.9.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", @@ -72,42 +72,6 @@ "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/xubaiw/CMark.lean", - "type": "git", - "subDir": null, - "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05", - "name": "CMark", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "rev": "effd8b8771cfd7ece69db99448168078e113c61f", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hargonix/LeanInk", - "type": "git", - "subDir": null, - "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f", - "name": "leanInk", - "manifestFile": "lake-manifest.json", - "inputRev": "doc-gen", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "rev": "b334278bbe691cb41af3e472ea0a85b6be81e98e", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, "configFile": "lakefile.lean"}], "name": "SphereEversion", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 3d453aac..17a3fdd0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ package «SphereEversion» where ⟨`relaxedAutoImplicit, false⟩] require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0" @[default_target] lean_lib «SphereEversion» where @@ -17,4 +17,4 @@ require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" meta if get_config? env = some "dev" then require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "main" \ No newline at end of file + "https://github.com/leanprover/doc-gen4" @ "main" diff --git a/lean-toolchain b/lean-toolchain index 78f39e21..4ef27c47 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc2 +leanprover/lean4:v4.9.0