From 41686a807058bf90d7558bb7f080193077349204 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 16 Feb 2024 00:59:00 +0100 Subject: [PATCH] chore: minimize more imports - InteractiveExpr doesn't exist; remove that commented import. - Remove two duplicate lines (presumably from a merge conflict). - Minimize open's in InductiveConstruction. --- SphereEversion/Global/Immersion.lean | 3 --- SphereEversion/Global/OneJetBundle.lean | 1 - SphereEversion/Global/SmoothEmbedding.lean | 17 +++++++---------- SphereEversion/InductiveConstructions.lean | 7 ++----- 4 files changed, 9 insertions(+), 19 deletions(-) diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index fd3b321a..f13aa5fa 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -4,9 +4,6 @@ import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation import SphereEversion.Global.Gromov import SphereEversion.Global.TwistOneJetSec --- import interactive_expr --- import interactive_expr --- set_option trace.filter_inst_type true -- set_option trace.filter_inst_type true noncomputable section diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 983e89c6..69e1d693 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -11,7 +11,6 @@ import Mathlib.Analysis.NormedSpace.Completion import Mathlib.Geometry.Manifold.Algebra.Monoid import Mathlib.Geometry.Manifold.ContMDiffMFDeriv import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc --- import SphereEversion.InteractiveExpr /-! # 1-jet bundles diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 5f0699f4..5b66363a 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -1,15 +1,12 @@ -import Mathlib.Topology.MetricSpace.HausdorffDistance -import Mathlib.Topology.NhdsSet -import Mathlib.Topology.UniformSpace.Separation -import Mathlib.Geometry.Manifold.ChartedSpace -import Mathlib.Geometry.Manifold.ContMDiffMFDeriv -import SphereEversion.Notations import SphereEversion.Indexing -import SphereEversion.ToMathlib.Topology.Paracompact -import SphereEversion.ToMathlib.Topology.Algebra.Order.Compact -import SphereEversion.ToMathlib.Topology.Misc -import SphereEversion.ToMathlib.Geometry.Manifold.SmoothManifoldWithCorners +import SphereEversion.Notations import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc +import SphereEversion.ToMathlib.Geometry.Manifold.SmoothManifoldWithCorners +import SphereEversion.ToMathlib.Topology.Misc +import SphereEversion.ToMathlib.Topology.Paracompact +import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions +import Mathlib.Order.Filter.Basic + noncomputable section diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 7e0bc681..1df05c75 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -1,16 +1,13 @@ -import SphereEversion.ToMathlib.Data.Set.Prod -import SphereEversion.ToMathlib.Data.Set.Lattice import SphereEversion.ToMathlib.Topology.Germ import SphereEversion.ToMathlib.Topology.Misc -import SphereEversion.ToMathlib.Order.Filter.Basic +import SphereEversion.ToMathlib.Data.Set.Lattice import SphereEversion.Indexing import SphereEversion.Notations --- import SphereEversion.InteractiveExpr -- import Mathlib.Tactic.Induction -- set_option trace.filter_inst_type true -open Set Filter Prod TopologicalSpace Function +open Set Filter Function open scoped Topology unitInterval