[Merged by Bors] - chore(Topology/Instances/*Real): organize instances by class#22562
Closed
Vierkantor wants to merge 8 commits intomasterfrom
Closed
[Merged by Bors] - chore(Topology/Instances/*Real): organize instances by class#22562Vierkantor wants to merge 8 commits intomasterfrom
Vierkantor wants to merge 8 commits intomasterfrom
Conversation
Currently, `Topology/Instances` has files defining topological instances on various types, organized by the type the instance is defined on. This PR takes the `E?(NN)?Real` instances and organizes them instead by the class that the instance belongs to (and puts all the Real-derived types together). Restructuring in this way should hopefully allow us to work with simpler concepts while not having to define more advanced concepts at the same time. I want to make a follow-up PR reorganizing the lemmas in similar ways. This change was discussed in the comments for #22093: #22093 (comment) Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Importing.20ENNReal.20in.20normed.20groups
PR summary 5c446139cc
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Instances.ENNReal.Defs | 1137 | 0 | -1137 (-100.00%) |
| Mathlib.Topology.Instances.EReal.Defs | 1043 | 0 | -1043 (-100.00%) |
| Mathlib.Topology.Instances.NNReal.Defs | 1132 | 0 | -1132 (-100.00%) |
| Mathlib.Topology.Instances.Real.Defs | 1121 | 0 | -1121 (-100.00%) |
| Mathlib.MeasureTheory.OuterMeasure.Defs | 1141 | 1022 | -119 (-10.43%) |
| Mathlib.Order.Filter.ENNReal | 1142 | 1084 | -58 (-5.08%) |
| Mathlib.Analysis.Subadditive | 1122 | 1133 | +11 (+0.98%) |
| Mathlib.Topology.Instances.CantorSet | 1122 | 1133 | +11 (+0.98%) |
| Mathlib.Topology.UnitInterval | 1125 | 1136 | +11 (+0.98%) |
| Mathlib.Topology.Instances.Rat | 1126 | 1137 | +11 (+0.98%) |
| Mathlib.Topology.UniformSpace.CompareReals | 1132 | 1142 | +10 (+0.88%) |
| Mathlib.Analysis.Normed.Group.Continuity | 1171 | 1163 | -8 (-0.68%) |
| Mathlib.Analysis.Convex.Topology | 1339 | 1346 | +7 (+0.52%) |
| Mathlib.Analysis.Normed.Group.Lemmas | 1303 | 1300 | -3 (-0.23%) |
| Mathlib.Analysis.Normed.Field.Lemmas | 1367 | 1364 | -3 (-0.22%) |
| Mathlib.Topology.Instances.EReal.Lemmas | 1235 | 1233 | -2 (-0.16%) |
| Mathlib.AlgebraicTopology.TopologicalSimplex | 1274 | 1273 | -1 (-0.08%) |
| Mathlib.Topology.Bornology.BoundedOperation | 1368 | 1367 | -1 (-0.07%) |
| Mathlib.Topology.MetricSpace.Perfect | 1372 | 1371 | -1 (-0.07%) |
| Mathlib.Topology.CWComplex.Classical.Basic | 1416 | 1415 | -1 (-0.07%) |
| Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable | 1449 | 1448 | -1 (-0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Topology.Instances.ENNReal.Defs |
-1137 |
Mathlib.Topology.Instances.NNReal.Defs |
-1132 |
Mathlib.Topology.Instances.Real.Defs |
-1121 |
Mathlib.Topology.Instances.EReal.Defs |
-1043 |
Mathlib.MeasureTheory.OuterMeasure.Defs |
-119 |
Mathlib.Order.Filter.ENNReal |
-58 |
3 filesMathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.Continuity Mathlib.Topology.Algebra.InfiniteSum.Field |
-8 |
Mathlib.Analysis.Normed.Group.NullSubmodule |
-7 |
Mathlib.AlgebraicTopology.SingularHomology.Basic |
-5 |
3 filesMathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.SpecialFunctions.Log.ERealExp |
-4 |
46 filesMathlib.Analysis.Convex.EGauge Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Field.Instances Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Operator.Compact Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.NormedSpace.BallAction Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.NormedSpace.Extr Mathlib.Analysis.NormedSpace.Int Mathlib.Analysis.NormedSpace.Real Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Analysis.Seminorm Mathlib.Data.Real.IsNonarchimedean Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Germ Mathlib.Topology.UniformSpace.Dini |
-3 |
342 filesMathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.CPolynomialDef Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.Order Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.Operations Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Hofer Mathlib.Analysis.Meromorphic.Basic Mathlib.Analysis.Meromorphic.Order Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.Convex Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Analysis.Normed.Group.Pointwise Mathlib.Analysis.Normed.Group.Quotient Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Convex Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Analysis.Normed.Ring.Units Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.SpecialFunctions.Choose Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecificLimits.Basic Mathlib.Analysis.SpecificLimits.Normed Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Data.Complex.Cardinality Mathlib.Data.Real.Cardinality Mathlib.Data.Real.Hyperreal Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.Conservative Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.FieldTheory.Galois.Profinite Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.ContMDiff.Constructions Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Geometry.Manifold.IsManifold.Basic Mathlib.Geometry.Manifold.IsManifold.ExtChartAt Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.Defs Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Pointwise Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.MeasureTheory.Measure.AddContent Mathlib.MeasureTheory.Measure.Comap Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.Count Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Map Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Sub Mathlib.MeasureTheory.Measure.Tight Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.OuterMeasure.OfAddContent Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.NumberTheory.EulerProduct.Basic Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.ProperSpace Mathlib.Probability.ConditionalProbability Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.Kernel Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.CompMap Mathlib.Probability.Kernel.Composition.CompNotation Mathlib.Probability.Kernel.Composition.CompProd Mathlib.Probability.Kernel.Composition.Comp Mathlib.Probability.Kernel.Composition.MapComap Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.Composition.Prod Mathlib.Probability.Kernel.Defs Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.Probability.UniformOn Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.ContinuousMap.Units Mathlib.Topology.Instances.EReal.Lemmas Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.MetricSpace.Contracting Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Topology.MetricSpace.PiNat Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.Topology.MetricSpace.Thickening Mathlib.Topology.Metrizable.Urysohn Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.PartitionOfUnity Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.Separation.NotNormal Mathlib.Topology.TietzeExtension Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.Hom |
-2 |
318 filesMathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Asymptotics.ExpGrowth Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.Isometry Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Continuous Mathlib.Analysis.InnerProductSpace.Convex Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.AbsConvexOpen Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Matrix Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Ring.FiniteExtension Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.Normed.Ring.SmoothingSeminorm Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Analysis.NormedSpace.Connected Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.NormedSpace.RCLike Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.PosLog Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Data.Complex.ExponentialBounds Mathlib.Data.Complex.FiniteDimensional Mathlib.Data.Real.Pi.Bounds Mathlib.Dynamics.Ergodic.Function Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.VectorField Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.MeasureTheory.Function.Egorov Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Integral.Indicator Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic Mathlib.MeasureTheory.Measure.Complex Mathlib.MeasureTheory.Measure.Doubling Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.NumberTheory.MulChar.Lemmas Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.NumberTheory.VonMangoldt Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Tactic.FunProp.ContDiff Mathlib.Tactic.FunProp.Differentiable Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.Instances.Complex Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Topology.MetricSpace.Perfect |
-1 |
42 filesMathlib.Algebra.Star.CHSH Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Data.Real.GoldenRatio Mathlib.Data.Real.Irrational Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.Pell Mathlib.NumberTheory.Rayleigh Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.Instances.Irrational Mathlib.Topology.Instances.NNReal.Lemmas Mathlib.Topology.Instances.RatLemmas |
1 |
61 filesMathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.NormedSpace.Extend Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Data.Real.StarOrdered Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ZetaValues Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps |
2 |
35 filesMathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.Module.CharacterModule Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.RCLike.Basic Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.LinearAlgebra.LinearDisjoint Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.AddCircle |
3 |
16 filesMathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Analysis.SumOverResidueClass Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.Topology.Instances.ENNReal.Lemmas Mathlib.Topology.Semicontinuous |
4 |
22 filesMathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.IntegerCompl Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Convex.Strong Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.Normed.Group.Rat Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.Identities Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.NumberTheory.Modular Mathlib.Topology.Instances.Real.Lemmas Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.MetricSpace.Completion |
5 |
61 filesMathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Analysis.Convex.TotallyBounded Mathlib.FieldTheory.LinearDisjoint Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.Locus |
6 |
3 filesMathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.Convex.Topology Mathlib.Topology.Algebra.Module.LocallyConvex |
7 |
Mathlib.Geometry.Manifold.Sheaf.Basic |
8 |
8 filesMathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.PathConnected Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Path |
9 |
Mathlib.Topology.UniformSpace.CompareReals |
10 |
4 filesMathlib.Analysis.Subadditive Mathlib.Topology.Instances.CantorSet Mathlib.Topology.Instances.Rat Mathlib.Topology.UnitInterval |
11 |
Mathlib.Topology.Algebra.Star.Real (new file) |
968 |
Mathlib.Topology.UniformSpace.Real (new file) |
990 |
Mathlib.Topology.Order.Real (new file) |
1014 |
Mathlib.Topology.Metrizable.Real (new file) |
1019 |
Mathlib.Topology.MetricSpace.ProperSpace.Real (new file) |
1029 |
Mathlib.Topology.Algebra.Ring.Real (new file) |
1132 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
YaelDillies
reviewed
Mar 4, 2025
Contributor
YaelDillies
left a comment
There was a problem hiding this comment.
merge merge merge :D
2 tasks
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
I was looking at `OuterMeasure.Defs`, which has a whole bunch of grey in its import graph, so I figured a bit of further restructuring could help. But looks like changing that didn't really help the import graph. This reverts commit 6980465.
grunweg
reviewed
Mar 5, 2025
Contributor
grunweg
left a comment
There was a problem hiding this comment.
I see you're actively working on this. I have some comments in the mean-time, and will return to this once you've finished your current edits. Looks great so far!
Contributor
Author
|
Hmm, there's still a large grey chunk of imports for |
Contributor
|
So, this is ready for review now? |
Vierkantor
commented
Mar 5, 2025
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Contributor
Author
Yes, I think I addressed everything. :) |
grunweg
reviewed
Mar 5, 2025
Contributor
grunweg
left a comment
There was a problem hiding this comment.
A few more comments on the module doc-strings.
| theorem continuous_coe : Continuous ((↑) : ℝ≥0 → ℝ) := | ||
| continuous_subtype_val | ||
|
|
||
| /-- Embedding of `ℝ≥0` to `ℝ` as a bundled continuous map. -/ |
Contributor
There was a problem hiding this comment.
Pre-existing, but while we're at it:
Suggested change
| /-- Embedding of `ℝ≥0` to `ℝ` as a bundled continuous map. -/ | |
| /-- Embedding of `ℝ≥0` to `ℝ` as a bundled continuous map -/ |
Contributor
There was a problem hiding this comment.
I would actually tend to add the period?
Contributor
There was a problem hiding this comment.
Well, the comment is not a complete sentence (merely a header), so should not have a period. This is even in the style guide: https://leanprover-community.github.io/contribute/doc.html#doc-strings
If a doc string is a complete sentence, then it should end in a period.
Contributor
There was a problem hiding this comment.
Then the style guide doesn't say anything about non-complete sentences, no?
Contributor
Author
There was a problem hiding this comment.
What if we split the difference? :)
Suggested change
| /-- Embedding of `ℝ≥0` to `ℝ` as a bundled continuous map. -/ | |
| /-- Embed `ℝ≥0` into `ℝ` as a bundled continuous map. -/ |
Contributor
There was a problem hiding this comment.
I view the style guide as an "iff" rule - but I also agree with the suggestion :-)
Contributor
|
Thanks a lot for taking on this refactoring. The previous design was not exactly import-minimal (and any ad hoc splittings were unsatisfying): this is a much more principled fix. There is a small import increase in some files; I think the other files offset this by a lot. The clearer structure will be worth it in the long term. maintainer delegate |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
This was referenced Mar 5, 2025
Vierkantor
commented
Mar 5, 2025
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
grunweg
reviewed
Mar 5, 2025
Member
|
Thanks 🎉 bors merge |
Contributor
|
Canceled. |
Contributor
|
Fixed the merge conflict. Assuming CI passes, can e.g. @Vierkantor or @jcommelin re-bors this, please? |
grunweg
added a commit
that referenced
this pull request
Mar 5, 2025
Splitting it out in #21554 was motivated by avoiding imports of ENNReal. This motivation has become moot now: - with #22562, just the basic properties of ENNReal do not add that many further imports - after #21670, Normed/Group/Basic.lean will import ENNReal anyway. Adding to this, the split into Basic and Continuity was never really clear in terms of imports: Basic.lean should be split further, but this does not seem like a good splitting boundary. While at it, replace one 'open' that has been likely mis-ported by 'open scoped'.
|
As this PR is labelled bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 5, 2025
Currently, `Topology/Instances` has files defining topological instances on various types, organized by the type the instance is defined on. This PR takes the `E?(NN)?Real` instances and organizes them instead by the class that the instance belongs to (and puts all the Real-derived types together). Restructuring in this way should hopefully allow us to work with simpler concepts while not having to define more advanced concepts at the same time. I want to make a follow-up PR reorganizing the lemmas in similar ways. This change was discussed in the comments for #22093: #22093 (comment) Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Importing.20ENNReal.20in.20normed.20groups Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
grunweg
added a commit
that referenced
this pull request
Mar 5, 2025
Splitting it out in #21554 was motivated by avoiding imports of ENNReal. This motivation has become moot now: - with #22562, just the basic properties of ENNReal do not add that many further imports - after #21670, Normed/Group/Basic.lean will import ENNReal anyway. Adding to this, the split into Basic and Continuity was never really clear in terms of imports: Basic.lean should be split further, but this does not seem like a good splitting boundary. While at it, replace one 'open' that has been likely mis-ported by 'open scoped'.
1 task
imbrem
pushed a commit
that referenced
this pull request
Mar 6, 2025
Currently, `Topology/Instances` has files defining topological instances on various types, organized by the type the instance is defined on. This PR takes the `E?(NN)?Real` instances and organizes them instead by the class that the instance belongs to (and puts all the Real-derived types together). Restructuring in this way should hopefully allow us to work with simpler concepts while not having to define more advanced concepts at the same time. I want to make a follow-up PR reorganizing the lemmas in similar ways. This change was discussed in the comments for #22093: #22093 (comment) Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Importing.20ENNReal.20in.20normed.20groups Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Currently,
Topology/Instanceshas files defining topological instances on various types, organized by the type the instance is defined on. This PR takes theE?(NN)?Realinstances and organizes them instead by the class that the instance belongs to (and puts all the Real-derived types together). Restructuring in this way should hopefully allow us to work with simpler concepts while not having to define more advanced concepts at the same time.I want to make a follow-up PR reorganizing the lemmas in similar ways.
This change was discussed in the comments for #22093: #22093 (comment)
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Importing.20ENNReal.20in.20normed.20groups