-
Notifications
You must be signed in to change notification settings - Fork 12
/
Copy pathSphereEversion.lean
64 lines (64 loc) · 3.13 KB
/
SphereEversion.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
import SphereEversion.Global.Gromov
import SphereEversion.Global.Immersion
import SphereEversion.Global.Localisation
import SphereEversion.Global.LocalisationData
import SphereEversion.Global.LocalizedConstruction
import SphereEversion.Global.OneJetBundle
import SphereEversion.Global.OneJetSec
import SphereEversion.Global.ParametricityForFree
import SphereEversion.Global.Relation
import SphereEversion.Global.SmoothEmbedding
import SphereEversion.Global.TwistOneJetSec
import SphereEversion.Indexing
import SphereEversion.InductiveConstructions
import SphereEversion.Local.AmpleRelation
import SphereEversion.Local.Corrugation
import SphereEversion.Local.DualPair
import SphereEversion.Local.HPrinciple
import SphereEversion.Local.OneJet
import SphereEversion.Local.ParametricHPrinciple
import SphereEversion.Local.Relation
import SphereEversion.Local.SphereEversion
import SphereEversion.Loops.Basic
import SphereEversion.Loops.DeltaMollifier
import SphereEversion.Loops.Exists
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.AddTorsor.AffineMap
import SphereEversion.ToMathlib.Analysis.ContDiff
import SphereEversion.ToMathlib.Analysis.Convex.Basic
import SphereEversion.ToMathlib.Analysis.CutOff
import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct
import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual
import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection
import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
import SphereEversion.ToMathlib.Analysis.Normed.Module.FiniteDimension
import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod
import SphereEversion.ToMathlib.Data.Nat.Basic
import SphereEversion.ToMathlib.Data.Set.Lattice
import SphereEversion.ToMathlib.Equivariant
import SphereEversion.ToMathlib.ExistsOfConvex
import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
import SphereEversion.ToMathlib.Geometry.Manifold.Immersion
import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable
import SphereEversion.ToMathlib.Geometry.Manifold.MiscManifold
import SphereEversion.ToMathlib.Geometry.Manifold.SmoothManifoldWithCorners
import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
import SphereEversion.ToMathlib.LinearAlgebra.Basic
import SphereEversion.ToMathlib.LinearAlgebra.FiniteDimensional
import SphereEversion.ToMathlib.MeasureTheory.BorelSpace
import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral
import SphereEversion.ToMathlib.Order.Filter.Basic
import SphereEversion.ToMathlib.Partition
import SphereEversion.ToMathlib.SmoothBarycentric
import SphereEversion.ToMathlib.Topology.Algebra.Module
import SphereEversion.ToMathlib.Topology.Misc
import SphereEversion.ToMathlib.Topology.Paracompact
import SphereEversion.ToMathlib.Topology.Path
import SphereEversion.ToMathlib.Topology.Separation.Hausdorff
import SphereEversion.ToMathlib.Unused.Fin