diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean index 30811a11..71e247fe 100644 --- a/SphereEversion/Global/Gromov.lean +++ b/SphereEversion/Global/Gromov.lean @@ -1,7 +1,9 @@ -import SphereEversion.Global.LocalisationData -import SphereEversion.Global.LocalizedConstruction -import SphereEversion.Global.ParametricityForFree -import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable +module + +public import SphereEversion.Global.LocalisationData +public import SphereEversion.Global.LocalizedConstruction +public import SphereEversion.Global.ParametricityForFree +public import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable /-! # Gromov's theorem @@ -9,6 +11,8 @@ import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable We prove the h-principle for open and ample first order differential relations. -/ +public section + noncomputable section diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index bec87cc3..437119c9 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -1,10 +1,14 @@ -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.Global.Gromov -import SphereEversion.Global.TwistOneJetSec +module + +public import Mathlib.Analysis.Convex.AmpleSet +public import Mathlib.Geometry.Manifold.Instances.Sphere +public import SphereEversion.ToMathlib.LinearAlgebra.FiniteDimensional +public import SphereEversion.ToMathlib.Geometry.Manifold.Immersion +public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation +public import SphereEversion.Global.Gromov +public import SphereEversion.Global.TwistOneJetSec + +@[expose] public section -- set_option trace.filter_inst_type true noncomputable section diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean index 90b43126..92b21c4c 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -1,5 +1,7 @@ -import SphereEversion.Local.AmpleRelation -import SphereEversion.Global.Relation +module + +public import SphereEversion.Local.AmpleRelation +public import SphereEversion.Global.Relation /-! # Link with the local story @@ -8,6 +10,8 @@ This file bridges the gap between Chapter 2 and Chapter 3. It builds on is about embedding any manifold into another one). -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean index 2be6fd33..4208c2db 100644 --- a/SphereEversion/Global/LocalisationData.lean +++ b/SphereEversion/Global/LocalisationData.lean @@ -1,5 +1,9 @@ -import Mathlib.Topology.MetricSpace.PartitionOfUnity -import SphereEversion.Global.SmoothEmbedding +module + +public import Mathlib.Topology.MetricSpace.PartitionOfUnity +public import SphereEversion.Global.SmoothEmbedding + +@[expose] public section noncomputable section diff --git a/SphereEversion/Global/LocalizedConstruction.lean b/SphereEversion/Global/LocalizedConstruction.lean index 0e7a6228..3e50bd74 100644 --- a/SphereEversion/Global/LocalizedConstruction.lean +++ b/SphereEversion/Global/LocalizedConstruction.lean @@ -1,5 +1,9 @@ -import SphereEversion.Global.Localisation -import SphereEversion.Local.HPrinciple +module + +public import SphereEversion.Global.Localisation +public import SphereEversion.Local.HPrinciple + +public section noncomputable section diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index ec4bb754..8f1053dd 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -5,16 +5,18 @@ Authors: Patrick Massot, Floris van Doorn ! This file was ported from Lean 3 source module global.one_jet_bundle -/ -import Mathlib.Tactic.Common +module -import Mathlib.Analysis.Normed.Module.Completion -import Mathlib.Geometry.Manifold.Algebra.Monoid -import Mathlib.Geometry.Manifold.ContMDiffMFDeriv -import Mathlib.Geometry.Manifold.Notation -import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc -import Mathlib.Geometry.Manifold.VectorBundle.Hom -import Mathlib.Geometry.Manifold.VectorBundle.Pullback -import Mathlib.Tactic.Monotonicity.Lemmas +public import Mathlib.Tactic.Common + +public import Mathlib.Analysis.Normed.Module.Completion +public import Mathlib.Geometry.Manifold.Algebra.Monoid +public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv +public import Mathlib.Geometry.Manifold.Notation +public import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc +public import Mathlib.Geometry.Manifold.VectorBundle.Hom +public import Mathlib.Geometry.Manifold.VectorBundle.Pullback +public import Mathlib.Tactic.Monotonicity.Lemmas /-! # 1-jet bundles @@ -31,6 +33,8 @@ We prove are smooth, then so is `x ↦ (f₁ x, f₃ x, ϕ₂ x ∘ ϕ₁ x) : N → J¹(M₁, M₃)`. -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index be812fa7..9be0658a 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -5,10 +5,12 @@ Authors: Patrick Massot, Floris van Doorn ! This file was ported from Lean 3 source module global.one_jet_sec -/ -import Mathlib.Order.Filter.Germ.Basic -import Mathlib.Geometry.Manifold.Notation -import SphereEversion.ToMathlib.Topology.Algebra.Module -import SphereEversion.Global.OneJetBundle +module + +public import Mathlib.Order.Filter.Germ.Basic +public import Mathlib.Geometry.Manifold.Notation +public import SphereEversion.ToMathlib.Topology.Algebra.Module +public import SphereEversion.Global.OneJetBundle /-! # Sections of 1-jet bundles @@ -23,6 +25,8 @@ In this file we consider two manifolds `M` and `M'` with models `I` and `I'` * `OneJetSet I M I' M'`: smooth sections of `OneJetBundle I M I' M' → M` -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index 65fa455d..4d34139d 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -1,5 +1,9 @@ -import SphereEversion.Global.Relation -import Mathlib.Analysis.Convex.AmpleSet +module + +public import SphereEversion.Global.Relation +public import Mathlib.Analysis.Convex.AmpleSet + +@[expose] public section noncomputable section diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index fc6da8ce..facdbab1 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -1,8 +1,10 @@ -import Mathlib.Geometry.Manifold.Metrizable -import SphereEversion.Local.DualPair -import SphereEversion.Global.OneJetSec -import SphereEversion.Global.SmoothEmbedding -import Mathlib.Analysis.Convex.AmpleSet +module + +public import Mathlib.Geometry.Manifold.Metrizable +public import SphereEversion.Local.DualPair +public import SphereEversion.Global.OneJetSec +public import SphereEversion.Global.SmoothEmbedding +public import Mathlib.Analysis.Convex.AmpleSet /-! # First order partial differential relations for maps between manifolds @@ -16,6 +18,7 @@ for maps from `M` to `M'` is a set in the 1-jet bundle J¹(M, M'), also known as `OneJetBundle I M I' M'`. -/ +@[expose] public section noncomputable section diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 9be52199..25f6564e 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -1,14 +1,18 @@ -import Mathlib.Analysis.Normed.Order.Lattice -import Mathlib.Geometry.Manifold.ContMDiff.Atlas -import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace -import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions -import Mathlib.Geometry.Manifold.Notation -import SphereEversion.Indexing -import SphereEversion.Notations -import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc -import SphereEversion.ToMathlib.Geometry.Manifold.IsManifold.ExtChartAt -import SphereEversion.ToMathlib.Topology.Misc -import SphereEversion.ToMathlib.Topology.Paracompact +module + +public import Mathlib.Analysis.Normed.Order.Lattice +public import Mathlib.Geometry.Manifold.ContMDiff.Atlas +public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace +public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions +public import Mathlib.Geometry.Manifold.Notation +public import SphereEversion.Indexing +public import SphereEversion.Notations +public import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc +public import SphereEversion.ToMathlib.Geometry.Manifold.IsManifold.ExtChartAt +public import SphereEversion.ToMathlib.Topology.Misc +public import SphereEversion.ToMathlib.Topology.Paracompact + +@[expose] public section noncomputable section diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index 8ad573eb..99ffb483 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -5,7 +5,11 @@ Authors: Heather Macbeth ! This file was ported from Lean 3 source module global.twist_one_jet_sec -/ -import SphereEversion.Global.OneJetSec +module + +public import SphereEversion.Global.OneJetSec + +@[expose] public section noncomputable section diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean index 158dda6e..032d4ab1 100644 --- a/SphereEversion/Indexing.lean +++ b/SphereEversion/Indexing.lean @@ -1,9 +1,11 @@ -import Mathlib.Order.Interval.Finset.Fin -import Mathlib.Data.Fin.SuccPredOrder -import Mathlib.Data.Nat.SuccPred -import Mathlib.SetTheory.Cardinal.Basic -import Mathlib.Tactic.Cases -import SphereEversion.ToMathlib.Data.Nat.Basic +module + +public import Mathlib.Order.Interval.Finset.Fin +public import Mathlib.Data.Fin.SuccPredOrder +public import Mathlib.Data.Nat.SuccPred +public import Mathlib.SetTheory.Cardinal.Basic +public import Mathlib.Tactic.Cases +public import SphereEversion.ToMathlib.Data.Nat.Basic /-! # Indexing types @@ -12,6 +14,8 @@ This file introduces `IndexType : ℕ → Type` such that `IndexType 0 = ℕ` an together with supporting lemmas. -/ +@[expose] public section + open Fin Set diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index bacf5d40..ee4ae08f 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -1,9 +1,13 @@ -import Mathlib.Topology.Germ -import Mathlib.Analysis.Complex.Norm -import Mathlib.Analysis.RCLike.Basic -import SphereEversion.ToMathlib.Topology.Misc -import SphereEversion.Indexing -import SphereEversion.Notations +module + +public import Mathlib.Topology.Germ +public import Mathlib.Analysis.Complex.Norm +public import Mathlib.Analysis.RCLike.Basic +public import SphereEversion.ToMathlib.Topology.Misc +public import SphereEversion.Indexing +public import SphereEversion.Notations + +@[expose] public section -- set_option trace.filter_inst_type true diff --git a/SphereEversion/Local/AmpleRelation.lean b/SphereEversion/Local/AmpleRelation.lean index b25dbc82..ef717293 100644 --- a/SphereEversion/Local/AmpleRelation.lean +++ b/SphereEversion/Local/AmpleRelation.lean @@ -3,9 +3,11 @@ Copyright (c) 2021 Patrick Massot. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Patrick Massot -/ -import Mathlib.Analysis.Convex.AmpleSet -import SphereEversion.Local.DualPair -import SphereEversion.Local.Relation +module + +public import Mathlib.Analysis.Convex.AmpleSet +public import SphereEversion.Local.DualPair +public import SphereEversion.Local.Relation /-! # Slices of first order relations @@ -27,6 +29,8 @@ order relations: a relation is ample if all its slices are ample sets. At the end of the file we consider 1-jet sections and slices corresponding to points in their image. -/ +@[expose] public section + variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean index 4a42ec65..de39ff70 100644 --- a/SphereEversion/Local/Corrugation.lean +++ b/SphereEversion/Local/Corrugation.lean @@ -1,11 +1,13 @@ -import Mathlib.Analysis.Asymptotics.Lemmas -import Mathlib.LinearAlgebra.Dual.Lemmas -import Mathlib.Analysis.Calculus.ParametricIntegral -import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic -import SphereEversion.ToMathlib.Algebra.Ring.Periodic -import SphereEversion.ToMathlib.MeasureTheory.BorelSpace -import SphereEversion.Loops.Basic -import SphereEversion.Local.DualPair +module + +public import Mathlib.Analysis.Asymptotics.Lemmas +public import Mathlib.LinearAlgebra.Dual.Lemmas +public import Mathlib.Analysis.Calculus.ParametricIntegral +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic +public import SphereEversion.ToMathlib.Algebra.Ring.Periodic +public import SphereEversion.ToMathlib.MeasureTheory.BorelSpace +public import SphereEversion.Loops.Basic +public import SphereEversion.Local.DualPair /-! # Theillière's corrugation operation @@ -30,6 +32,8 @@ The main definition is `corrugation`. The main results are: -/ +@[expose] public section + noncomputable section open Set Function Filter MeasureTheory ContinuousLinearMap diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean index b8cce50e..74c0df2b 100644 --- a/SphereEversion/Local/DualPair.lean +++ b/SphereEversion/Local/DualPair.lean @@ -1,10 +1,12 @@ -import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension -import Mathlib.Analysis.Complex.Norm -import Mathlib.Analysis.Normed.Module.Completion -import Mathlib.LinearAlgebra.Dual.Lemmas -import SphereEversion.Notations -import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod -import SphereEversion.ToMathlib.LinearAlgebra.Basic +module + +public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension +public import Mathlib.Analysis.Complex.Norm +public import Mathlib.Analysis.Normed.Module.Completion +public import Mathlib.LinearAlgebra.Dual.Lemmas +public import SphereEversion.Notations +public import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod +public import SphereEversion.ToMathlib.LinearAlgebra.Basic /-! # Dual pairs @@ -28,6 +30,8 @@ This is crucial in order to apply convex integration to immersions. Then we prove continuity and smoothness lemmas for this operation. -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index ed9d5c72..369f02b0 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -1,8 +1,10 @@ -import Mathlib.LinearAlgebra.Basis.Flag -import Mathlib.LinearAlgebra.FreeModule.PID -import SphereEversion.Loops.Exists -import SphereEversion.Local.Corrugation -import SphereEversion.Local.AmpleRelation +module + +public import Mathlib.LinearAlgebra.Basis.Flag +public import Mathlib.LinearAlgebra.FreeModule.PID +public import SphereEversion.Loops.Exists +public import SphereEversion.Local.Corrugation +public import SphereEversion.Local.AmpleRelation /-! # Local h-principle for open and ample relations @@ -50,6 +52,8 @@ need to access its components only once. -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean index 5857f207..5b2e1e18 100644 --- a/SphereEversion/Local/OneJet.lean +++ b/SphereEversion/Local/OneJet.lean @@ -1,6 +1,8 @@ -import Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Analysis.SpecialFunctions.SmoothTransition -import SphereEversion.Notations +module + +public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.Analysis.SpecialFunctions.SmoothTransition +public import SphereEversion.Notations /-! # Spaces of 1-jets and their sections @@ -22,6 +24,8 @@ more smoothness constraints at `t = 0` and `t = 1` (requiring flat functions), b for smooth concatenations anyway. -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean index 04059ca6..6be928bd 100644 --- a/SphereEversion/Local/ParametricHPrinciple.lean +++ b/SphereEversion/Local/ParametricHPrinciple.lean @@ -1,5 +1,7 @@ -import SphereEversion.Local.HPrinciple -import SphereEversion.ToMathlib.Topology.Algebra.Module +module + +public import SphereEversion.Local.HPrinciple +public import SphereEversion.ToMathlib.Topology.Algebra.Module /-! In this file we prove the parametric version of the local h-principle. @@ -14,6 +16,8 @@ then there exists a homotopy `𝓕 : ℝ × P → J¹(E, F)` between `𝓕` and near `K`, that agrees with `𝓕₀` near `C` and is everywhere `ε`-close to `𝓕₀` -/ +@[expose] public section + noncomputable section open Set Function RelLoc diff --git a/SphereEversion/Local/Relation.lean b/SphereEversion/Local/Relation.lean index 12e85441..6436314c 100644 --- a/SphereEversion/Local/Relation.lean +++ b/SphereEversion/Local/Relation.lean @@ -1,5 +1,7 @@ -import Mathlib.Topology.MetricSpace.HausdorffDistance -import SphereEversion.Local.OneJet +module + +public import Mathlib.Topology.MetricSpace.HausdorffDistance +public import SphereEversion.Local.OneJet /-! # Local partial differential relations and their formal solutions @@ -15,6 +17,8 @@ The h-principle question is whether we can deform any formal solution into a sol The type of deformations is `HtpyJetSet E F` (homotopies of 1-jet sections). -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index 7e351398..daf49543 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -1,7 +1,9 @@ -import Mathlib.Analysis.Convex.AmpleSet -import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation -import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual -import SphereEversion.Local.ParametricHPrinciple +module + +public import Mathlib.Analysis.Convex.AmpleSet +public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation +public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual +public import SphereEversion.Local.ParametricHPrinciple /-! This is file proves the existence of a sphere eversion from the local verson of the h-principle. @@ -20,6 +22,8 @@ Finally, we obtain the existence of sphere eversion from the parametric local h- proven in `Local/ParametricHPrinciple`. -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean index 5a7092b7..d9a708cb 100644 --- a/SphereEversion/Loops/Basic.lean +++ b/SphereEversion/Loops/Basic.lean @@ -1,11 +1,15 @@ -import SphereEversion.Notations -import SphereEversion.ToMathlib.Equivariant -import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral +module + +public import SphereEversion.Notations +public import SphereEversion.ToMathlib.Equivariant +public import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral /-! # Basic definitions and properties of loops -/ +@[expose] public section + open Set Function FiniteDimensional Int TopologicalSpace open scoped Topology unitInterval diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean index 3f79eb2a..d1f10e58 100644 --- a/SphereEversion/Loops/DeltaMollifier.lean +++ b/SphereEversion/Loops/DeltaMollifier.lean @@ -1,11 +1,13 @@ -import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct -import Mathlib.Analysis.Convolution -import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic -import Mathlib.MeasureTheory.Measure.Haar.Unique -import Mathlib.Analysis.Calculus.BumpFunction.Normed -import SphereEversion.ToMathlib.Algebra.Ring.Periodic -import SphereEversion.ToMathlib.Analysis.ContDiff -import SphereEversion.Loops.Basic +module + +public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct +public import Mathlib.Analysis.Convolution +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic +public import Mathlib.MeasureTheory.Measure.Haar.Unique +public import Mathlib.Analysis.Calculus.BumpFunction.Normed +public import SphereEversion.ToMathlib.Algebra.Ring.Periodic +public import SphereEversion.ToMathlib.Analysis.ContDiff +public import SphereEversion.Loops.Basic /-! # Delta mollifiers @@ -26,6 +28,8 @@ The key ingredients are the existence of smooth "bump functions" and a powerful convolutions. -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 7a66dde3..3afcadd8 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -1,6 +1,10 @@ -import SphereEversion.Loops.Reparametrization -import SphereEversion.ToMathlib.Analysis.CutOff -import Mathlib.Topology.MetricSpace.HausdorffDistance +module + +public import SphereEversion.Loops.Reparametrization +public import SphereEversion.ToMathlib.Analysis.CutOff +public import Mathlib.Topology.MetricSpace.HausdorffDistance + +public section noncomputable section diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 52c973a4..351c255a 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -1,11 +1,13 @@ -import Mathlib.Analysis.Calculus.BumpFunction.Convolution -import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct -import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts -import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic -import SphereEversion.Loops.Surrounding -import SphereEversion.Loops.DeltaMollifier -import SphereEversion.ToMathlib.ExistsOfConvex -import SphereEversion.ToMathlib.Analysis.ContDiff +module + +public import Mathlib.Analysis.Calculus.BumpFunction.Convolution +public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic +public import SphereEversion.Loops.Surrounding +public import SphereEversion.Loops.DeltaMollifier +public import SphereEversion.ToMathlib.ExistsOfConvex +public import SphereEversion.ToMathlib.Analysis.ContDiff /-! # The reparametrization lemma @@ -45,6 +47,8 @@ The key ingredients are theories of calculus, convex hulls, barycentric coordina existence of delta mollifiers, partitions of unity, and the inverse function theorem. -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index dff8128f..d70ce5db 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -1,10 +1,12 @@ -import SphereEversion.InductiveConstructions -import SphereEversion.Loops.Basic -import SphereEversion.ToMathlib.ExistsOfConvex -import SphereEversion.ToMathlib.SmoothBarycentric -import SphereEversion.ToMathlib.Topology.Path -import Mathlib.Analysis.Convex.Caratheodory -import Mathlib.Analysis.Normed.Module.FiniteDimension +module + +public import SphereEversion.InductiveConstructions +public import SphereEversion.Loops.Basic +public import SphereEversion.ToMathlib.ExistsOfConvex +public import SphereEversion.ToMathlib.SmoothBarycentric +public import SphereEversion.ToMathlib.Topology.Path +public import Mathlib.Analysis.Convex.Caratheodory +public import Mathlib.Analysis.Normed.Module.FiniteDimension /-! # Surrounding families of loops @@ -31,6 +33,8 @@ The key results are: * `exists_surrounding_loops` -/ +@[expose] public section + -- to obtain that normed spaces are locally connected open Set Function Module Int Prod Path Filter open scoped Topology unitInterval ContDiff diff --git a/SphereEversion/Main.lean b/SphereEversion/Main.lean index 4b838809..2c83edaa 100644 --- a/SphereEversion/Main.lean +++ b/SphereEversion/Main.lean @@ -1,4 +1,8 @@ -import SphereEversion.Global.Immersion +module + +public import SphereEversion.Global.Immersion + +public section open Metric FiniteDimensional Set ModelWithCorners diff --git a/SphereEversion/Notations.lean b/SphereEversion/Notations.lean index c0727f94..7f4adf89 100644 --- a/SphereEversion/Notations.lean +++ b/SphereEversion/Notations.lean @@ -1,4 +1,8 @@ -import Mathlib.Analysis.Calculus.ContDiff.Basic +module + +public import Mathlib.Analysis.Calculus.ContDiff.Basic + +public section open scoped Topology ContDiff diff --git a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean index 817ee571..b292864b 100644 --- a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean +++ b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean @@ -1,6 +1,8 @@ -import Mathlib.Analysis.Normed.Order.Lattice -import Mathlib.Algebra.Ring.Periodic -import Mathlib.Topology.Separation.Hausdorff +module + +public import Mathlib.Analysis.Normed.Order.Lattice +public import Mathlib.Algebra.Ring.Periodic +public import Mathlib.Topology.Separation.Hausdorff -- TODO: the file this references doesn't exist in mathlib any more; rename this one appropriately! @@ -21,6 +23,8 @@ Patrick is not sure this is the optimal version. In the first part, generalize many lemmas to any period and add to `Algebra.Ring.Periodic.lean`? -/ +@[expose] public section + noncomputable section diff --git a/SphereEversion/ToMathlib/Analysis/Calculus.lean b/SphereEversion/ToMathlib/Analysis/Calculus.lean index d8c43cd1..eb9d32d9 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus.lean @@ -1,6 +1,10 @@ -import Mathlib.Analysis.Normed.Module.Completion -import Mathlib.Analysis.SpecialFunctions.SmoothTransition -import SphereEversion.ToMathlib.Topology.Misc +module + +public import Mathlib.Analysis.Normed.Module.Completion +public import Mathlib.Analysis.SpecialFunctions.SmoothTransition +public import SphereEversion.ToMathlib.Topology.Misc + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean b/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean index cae80c77..a99b8166 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean @@ -1,4 +1,6 @@ -import Mathlib.Analysis.Calculus.AddTorsor.AffineMap +module + +public import Mathlib.Analysis.Calculus.AddTorsor.AffineMap /-! @@ -8,6 +10,8 @@ TODO Generalise these lemmas appropriately. -/ +public section + open Set Function Metric AffineMap diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean index 6da0e5b0..8313cf6b 100644 --- a/SphereEversion/ToMathlib/Analysis/ContDiff.lean +++ b/SphereEversion/ToMathlib/Analysis/ContDiff.lean @@ -1,10 +1,14 @@ -import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv -import Mathlib.Analysis.Calculus.ContDiff.Basic -import Mathlib.Analysis.Calculus.Deriv.MeanValue -import Mathlib.Analysis.InnerProductSpace.Calculus -import Mathlib.Analysis.InnerProductSpace.Dual -import SphereEversion.ToMathlib.Analysis.Calculus -import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod +module + +public import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv +public import Mathlib.Analysis.Calculus.ContDiff.Basic +public import Mathlib.Analysis.Calculus.Deriv.MeanValue +public import Mathlib.Analysis.InnerProductSpace.Calculus +public import Mathlib.Analysis.InnerProductSpace.Dual +public import SphereEversion.ToMathlib.Analysis.Calculus +public import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean index 54221a86..1120e1b5 100644 --- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean +++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean @@ -1,6 +1,10 @@ -import Mathlib.Analysis.Convex.Combination -import Mathlib.Algebra.Module.BigOperators -import Mathlib.Algebra.Order.Hom.Ring +module + +public import Mathlib.Analysis.Convex.Combination +public import Mathlib.Algebra.Module.BigOperators +public import Mathlib.Algebra.Order.Hom.Ring + +@[expose] public section open Function Set diff --git a/SphereEversion/ToMathlib/Analysis/CutOff.lean b/SphereEversion/ToMathlib/Analysis/CutOff.lean index d195cd29..e5a43f51 100644 --- a/SphereEversion/ToMathlib/Analysis/CutOff.lean +++ b/SphereEversion/ToMathlib/Analysis/CutOff.lean @@ -1,4 +1,8 @@ -import Mathlib.Geometry.Manifold.PartitionOfUnity +module + +public import Mathlib.Geometry.Manifold.PartitionOfUnity + +public section open Set Filter diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean index 88817fb1..45d3ca5f 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean @@ -3,12 +3,16 @@ Copyright (c) 2022 Heather Macbeth. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Heather Macbeth -/ -import Mathlib.Analysis.InnerProductSpace.Dual -import Mathlib.Analysis.InnerProductSpace.Orientation -import Mathlib.LinearAlgebra.Alternating.Curry +module + +public import Mathlib.Analysis.InnerProductSpace.Dual +public import Mathlib.Analysis.InnerProductSpace.Orientation +public import Mathlib.LinearAlgebra.Alternating.Curry /-! # The cross-product on an oriented real inner product space of dimension three -/ +public section + noncomputable section open scoped RealInnerProductSpace @@ -74,7 +78,7 @@ def crossProduct' : E →L[ℝ] E →L[ℝ] E := @[simp] theorem crossProduct'_apply (v : E) : ω.crossProduct' v = LinearMap.toContinuousLinearMap (ω.crossProduct v) := - rfl + (rfl) theorem norm_crossProduct (u : E) (v : (ℝ ∙ u)ᗮ) : ‖u×₃v‖ = ‖u‖ * ‖v‖ := by classical diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean index 965e58f6..21f0c3ef 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean @@ -1,5 +1,9 @@ -import Mathlib.Analysis.InnerProductSpace.Dual -import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection.Submodule +module + +public import Mathlib.Analysis.InnerProductSpace.Dual +public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection.Submodule + +public section open scoped RealInnerProductSpace diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean index 714ca6a5..83db98d0 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean @@ -1,4 +1,8 @@ -import Mathlib.Analysis.InnerProductSpace.Projection.Submodule +module + +public import Mathlib.Analysis.InnerProductSpace.Projection.Submodule + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean index e365eec5..bc1ddad0 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean @@ -5,13 +5,17 @@ Authors: Heather Macbeth ! This file was ported from Lean 3 source module to_mathlib.analysis.inner_product_space.rotation -/ -import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv -import SphereEversion.ToMathlib.Analysis.ContDiff -import SphereEversion.ToMathlib.LinearAlgebra.Basic -import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct +module + +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv +public import SphereEversion.ToMathlib.Analysis.ContDiff +public import SphereEversion.ToMathlib.LinearAlgebra.Basic +public import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct /-! # Rotation about an axis, considered as a function in that axis -/ +@[expose] public section + noncomputable section open scoped RealInnerProductSpace @@ -49,7 +53,7 @@ theorem rot_eq_aux : ω.rot = ω.rotAux := by ext1 p dsimp [rot, rotAux] rw [id_eq_sum_starProjection_self_orthogonalComplement (K := ℝ ∙ p.2)] - simp only [smul_add, sub_smul, one_smul, starProjection] + simp only [smul_add, sub_smul, one_smul, starProjection, crossProduct'_apply] abel /-- The map `rot` is smooth on `ℝ × (E \ {0})`. -/ diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean index 6bd50bb3..cc6882f0 100644 --- a/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean +++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean @@ -1,5 +1,9 @@ -import Mathlib.Analysis.InnerProductSpace.EuclideanDist -import Mathlib.Topology.OpenPartialHomeomorph.Constructions +module + +public import Mathlib.Analysis.InnerProductSpace.EuclideanDist +public import Mathlib.Topology.OpenPartialHomeomorph.Constructions + +@[expose] public section variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean index bb5aa8c6..ec7d3fc5 100644 --- a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean +++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean @@ -1,6 +1,10 @@ -import Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps -import Mathlib.Analysis.Normed.Operator.Prod +module + +public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps +public import Mathlib.Analysis.Normed.Operator.Prod + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Data/Nat/Basic.lean b/SphereEversion/ToMathlib/Data/Nat/Basic.lean index 7945d3f8..2611a014 100644 --- a/SphereEversion/ToMathlib/Data/Nat/Basic.lean +++ b/SphereEversion/ToMathlib/Data/Nat/Basic.lean @@ -1,6 +1,10 @@ -import Mathlib.Data.Nat.Notation -import Mathlib.Logic.Function.Basic -import Mathlib.Tactic.Choose +module + +public import Mathlib.Data.Nat.Notation +public import Mathlib.Logic.Function.Basic +public import Mathlib.Tactic.Choose + +public section -- The next lemma won't be used, it's a warming up exercise for the one below. -- It could go to mathlib. diff --git a/SphereEversion/ToMathlib/Equivariant.lean b/SphereEversion/ToMathlib/Equivariant.lean index 216fa200..28c7af13 100644 --- a/SphereEversion/ToMathlib/Equivariant.lean +++ b/SphereEversion/ToMathlib/Equivariant.lean @@ -1,5 +1,9 @@ -import Mathlib.Topology.Algebra.Order.Floor -import SphereEversion.ToMathlib.Topology.Misc +module + +public import Mathlib.Topology.Algebra.Order.Floor +public import SphereEversion.ToMathlib.Topology.Misc + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index d6e0f696..048904de 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -1,5 +1,9 @@ -import SphereEversion.ToMathlib.Partition -import Mathlib.Geometry.Manifold.Notation +module + +public import SphereEversion.ToMathlib.Partition +public import Mathlib.Geometry.Manifold.Notation + +public section noncomputable section diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean index 36e175a0..860b9fdb 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean @@ -3,20 +3,23 @@ Copyright (c) 2023 Patrick Massot. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Patrick Massot -/ +module -import Mathlib.Algebra.Ring.Subring.Order -import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions -import Mathlib.Geometry.Manifold.MFDeriv.Basic -import Mathlib.Geometry.Manifold.Notation -import Mathlib.Order.Filter.Ring -import Mathlib.Tactic.Cases -import Mathlib.Topology.Germ +public import Mathlib.Algebra.Ring.Subring.Order +public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions +public import Mathlib.Geometry.Manifold.MFDeriv.Basic +public import Mathlib.Geometry.Manifold.Notation +public import Mathlib.Order.Filter.Ring +public import Mathlib.Tactic.Cases +public import Mathlib.Topology.Germ /-! ## Germs of smooth functions under construction: might need further refactoring to be usable! -/ +@[expose] public section + -- TODO: please confirm authorship and copyright are appropriate noncomputable section diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean index 170ce05c..61e649fb 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean @@ -3,9 +3,11 @@ Copyright (c) 2024 Michael Rothgang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Rothgang -/ -import Mathlib.Geometry.Manifold.ContMDiff.Defs -import Mathlib.Geometry.Manifold.MFDeriv.Defs -import Mathlib.Geometry.Manifold.Notation +module + +public import Mathlib.Geometry.Manifold.ContMDiff.Defs +public import Mathlib.Geometry.Manifold.MFDeriv.Defs +public import Mathlib.Geometry.Manifold.Notation /-! ## Smooth immersions @@ -33,6 +35,8 @@ but in finite dimensions, the general definition is equivalent to the one in thi manifold, immersion -/ + +public section noncomputable section open Set Function diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index 9281516b..05520ae7 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -1,4 +1,8 @@ -import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt +module + +public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt + +@[expose] public section open scoped Topology diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean index 484d5884..bb4be091 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean @@ -1,4 +1,8 @@ -import Mathlib.Geometry.Manifold.Metrizable +module + +public import Mathlib.Geometry.Manifold.Metrizable + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean index e95f8727..08cea64e 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean @@ -5,13 +5,17 @@ Authors: Floris van Doorn ! This file was ported from Lean 3 source module to_mathlib.geometry.manifold.vector_bundle.misc -/ -import Mathlib.Geometry.Manifold.VectorBundle.Basic -import Mathlib.Topology.VectorBundle.Hom +module + +public import Mathlib.Geometry.Manifold.VectorBundle.Basic +public import Mathlib.Topology.VectorBundle.Hom /-! # Various operations on and properties of smooth vector bundles -/ +public section + noncomputable section open Bundle Set diff --git a/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean b/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean index 4101b697..c5b500ab 100644 --- a/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean +++ b/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean @@ -1,8 +1,12 @@ -import Mathlib.Algebra.Module.Submodule.Ker -import Mathlib.LinearAlgebra.Span.Defs +module + +public import Mathlib.Algebra.Module.Submodule.Ker +public import Mathlib.LinearAlgebra.Span.Defs /-! Note: some results should go to `LinearAlgebra.Span`. -/ +public section + open Submodule Function diff --git a/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean b/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean index 1f1cd90f..4cc56e1b 100644 --- a/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean +++ b/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean @@ -1,4 +1,8 @@ -import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +module + +public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas + +public section open Module Submodule diff --git a/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean b/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean index 5115b99f..57dff6c7 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/BorelSpace.lean @@ -1,4 +1,8 @@ -import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic +module + +public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic + +public section variable (X : Type*) [TopologicalSpace X] diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean index 65d80026..84f5def6 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -1,7 +1,11 @@ -import Mathlib.Analysis.Calculus.ParametricIntegral -import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension -import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus -import SphereEversion.ToMathlib.Analysis.Calculus +module + +public import Mathlib.Analysis.Calculus.ParametricIntegral +public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +public import SphereEversion.ToMathlib.Analysis.Calculus + +public section open TopologicalSpace MeasureTheory Filter FirstCountableTopology Metric Set Function open scoped Topology diff --git a/SphereEversion/ToMathlib/Order/Filter/Basic.lean b/SphereEversion/ToMathlib/Order/Filter/Basic.lean index 617feb19..936c919d 100644 --- a/SphereEversion/ToMathlib/Order/Filter/Basic.lean +++ b/SphereEversion/ToMathlib/Order/Filter/Basic.lean @@ -1,4 +1,8 @@ -import Mathlib.Order.Filter.Basic +module + +public import Mathlib.Order.Filter.Basic + +public section theorem Filter.EventuallyEq.eventuallyEq_ite {X Y : Type*} {l : Filter X} {f g : X → Y} {P : X → Prop} [DecidablePred P] (h : f =ᶠ[l] g) : diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean index 921df6bb..03135fb5 100644 --- a/SphereEversion/ToMathlib/Partition.lean +++ b/SphereEversion/ToMathlib/Partition.lean @@ -1,6 +1,10 @@ -import Mathlib.Geometry.Manifold.PartitionOfUnity -import SphereEversion.ToMathlib.Analysis.Convex.Basic -import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm +module + +public import Mathlib.Geometry.Manifold.PartitionOfUnity +public import SphereEversion.ToMathlib.Analysis.Convex.Basic +public import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean index f09e06fb..365ba03c 100644 --- a/SphereEversion/ToMathlib/SmoothBarycentric.lean +++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean @@ -1,7 +1,11 @@ -import Mathlib.Analysis.Calculus.AddTorsor.Coord -import Mathlib.Analysis.Matrix.Normed -import Mathlib.LinearAlgebra.AffineSpace.Matrix -import Mathlib.Tactic.Cases +module + +public import Mathlib.Analysis.Calculus.AddTorsor.Coord +public import Mathlib.Analysis.Matrix.Normed +public import Mathlib.LinearAlgebra.AffineSpace.Matrix +public import Mathlib.Tactic.Cases + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean index 7d0a3de3..2b4c8622 100644 --- a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean +++ b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean @@ -1,4 +1,8 @@ -import Mathlib.Topology.Algebra.Module.Equiv +module + +public import Mathlib.Topology.Algebra.Module.Equiv + +public section namespace ContinuousLinearMap diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index 54cf8cb7..b40cf2f3 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -1,9 +1,13 @@ -import Mathlib.Algebra.Ring.Periodic -import Mathlib.Analysis.Normed.Affine.Convex -import Mathlib.Tactic.Cases -import Mathlib.Topology.Algebra.Order.Floor -import Mathlib.Topology.EMetricSpace.Paracompact -import Mathlib.Topology.ShrinkingLemma +module + +public import Mathlib.Algebra.Ring.Periodic +public import Mathlib.Analysis.Normed.Affine.Convex +public import Mathlib.Tactic.Cases +public import Mathlib.Topology.Algebra.Order.Floor +public import Mathlib.Topology.EMetricSpace.Paracompact +public import Mathlib.Topology.ShrinkingLemma + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean index 9a8281b7..57e6871a 100644 --- a/SphereEversion/ToMathlib/Topology/Paracompact.lean +++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean @@ -1,6 +1,10 @@ -import Mathlib.Topology.Separation.Hausdorff -import Mathlib.Basic.Real.Basic -import Mathlib.Order.Interval.Finset.Nat +module + +public import Mathlib.Topology.Separation.Hausdorff +public import Mathlib.Basic.Real.Basic +public import Mathlib.Order.Interval.Finset.Nat + +public section open scoped Topology diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean index 604675e5..531ec5d0 100644 --- a/SphereEversion/ToMathlib/Topology/Path.lean +++ b/SphereEversion/ToMathlib/Topology/Path.lean @@ -1,6 +1,10 @@ -import Mathlib.Analysis.Normed.Field.Basic -import Mathlib.Analysis.Normed.Order.Lattice -import Mathlib.Topology.Connected.PathConnected +module + +public import Mathlib.Analysis.Normed.Field.Basic +public import Mathlib.Analysis.Normed.Order.Lattice +public import Mathlib.Topology.Connected.PathConnected + +@[expose] public section open Set Function diff --git a/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean b/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean index cd5c7a64..029d7fff 100644 --- a/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean +++ b/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean @@ -5,8 +5,10 @@ Authors: Floris van Doorn ! This file was ported from Lean 3 source module to_mathlib.unused.eventually_constant -/ -import Mathlib.Data.Nat.Lattice -import Mathlib.Topology.Separation.Hausdorff +module + +public import Mathlib.Data.Nat.Lattice +public import Mathlib.Topology.Separation.Hausdorff /-! # Eventually constant sequences @@ -14,6 +16,8 @@ import Mathlib.Topology.Separation.Hausdorff Related: `monotonic_sequence_limit_index` -/ +@[expose] public section + -- in mathlib, this should probably import -- import Order.Filter.atTop_bot diff --git a/SphereEversion/ToMathlib/Unused/Fin.lean b/SphereEversion/ToMathlib/Unused/Fin.lean index b06b17e4..cb21a9cf 100644 --- a/SphereEversion/ToMathlib/Unused/Fin.lean +++ b/SphereEversion/ToMathlib/Unused/Fin.lean @@ -1,4 +1,8 @@ -import Mathlib.Data.Fin.SuccPred +module + +public import Mathlib.Data.Fin.SuccPred + +public section -- not directly used theorem Fin.coe_succ_le_iff_le {n : ℕ} {j k : Fin n} : j.castSucc ≤ k.castSucc ↔ j ≤ k := diff --git a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean index 74a3522a..5916e6d3 100644 --- a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean +++ b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean @@ -1,6 +1,10 @@ -import Mathlib.Geometry.Manifold.VectorBundle.Tangent -import Mathlib.Geometry.Manifold.MFDeriv.Defs -import Mathlib.Analysis.Calculus.ContDiff.Defs +module + +public import Mathlib.Geometry.Manifold.VectorBundle.Tangent +public import Mathlib.Geometry.Manifold.MFDeriv.Defs +public import Mathlib.Analysis.Calculus.ContDiff.Defs + +public section open Bundle Set Function Filter ContinuousLinearMap diff --git a/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean b/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean index 9f8c2e56..43dde897 100644 --- a/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean +++ b/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean @@ -1,7 +1,11 @@ -import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic -import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus -import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts -import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic +module + +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic + +@[expose] public section noncomputable section diff --git a/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean b/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean index 4d036115..19b260c0 100644 --- a/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean +++ b/SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean @@ -1,4 +1,8 @@ -import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct +module + +public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct + +@[expose] public section /- Multilinear map stuff that was meant as preliminaries for smooth functions gluing.