feat(Topology): define ContinuousEval{,Const} classes

[urkud]

---

TODO

• Add docs
• Add similar typeclasses for UniformContinuous (optional)
• Add instances for
  • ContinuousMap
  • ContinuousMonoidHom
  • ContinuousMapZero
  • ContinuousLinearMap (added ContinuousEvalConst, we didn't have continuous_eval lemma).
  • ContinuousMultilinearMap
  • ContinuousAlternatingMap
  • non-instances assuming a continuous projection from F to F'.
• Deprecate type-specific lemmas.

[github-actions]

PR summary 4901e4e02f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
4 files Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Analysis.Normed.Operator.Compact	1
798 files Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.MeanInequalitiesPow Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.NumberTheory.Liouville.LiouvilleWith Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Topology.CompactOpen Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Analysis.Convex.AmpleSet Mathlib.Probability.Variance Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.MulChar.Lemmas Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Tactic.FunProp.ContDiff Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Topology.Homotopy.Contractible Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Analysis.Calculus.Deriv.Add Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.NumberTheory.GaussSum Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Topology.UniformSpace.Ascoli Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Topology.ContinuousMap.Polynomial Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Flat.Basic Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Instances.Real Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.Convex.Topology Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Convex.Side Mathlib.MeasureTheory.Function.L2Space Mathlib.Topology.VectorBundle.Hom Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Analysis.NormedSpace.RCLike Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Condensed.Light.Explicit Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Probability.Kernel.Composition Mathlib.NumberTheory.Liouville.LiouvilleNumber Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Probability.Martingale.OptionalSampling Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Convex.GaugeRescale Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.Discriminant Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Condensed.Light.CartesianClosed Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Analysis.InnerProductSpace.Dual Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Calculus.SmoothSeries Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.AlgebraicGeometry.Spec Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Analysis.Calculus.TangentCone Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.AlgebraicGeometry.ResidueField Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ClopenBox Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Topology.Instances.AddCircle Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Topology.Homotopy.Path Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Analysis.Calculus.Taylor Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.MeasureTheory.Integral.Bochner Mathlib.Condensed.Discrete.LocallyConstant Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Probability.Martingale.Basic Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Topology.Homotopy.Basic Mathlib.NumberTheory.LSeries.Basic Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.Topology.UrysohnsBounded Mathlib.AlgebraicGeometry.Properties Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Topology.Homotopy.Product Mathlib.Data.Real.Pi.Irrational Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Topology.Metrizable.Urysohn Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.RingTheory.Flat.Algebra Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Probability.Kernel.IntegralCompProd Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.Condensed.Discrete.Module Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Topology.ContinuousMap.Bounded Mathlib.Analysis.InnerProductSpace.Basic Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Analysis.Complex.OperatorNorm Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Probability.Kernel.Disintegration.Density Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.MeasureTheory.Constructions.Prod.Integral Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.Condensed.Light.Epi Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.PartitionOfUnity Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.Data.Real.Pi.Leibniz Mathlib.NumberTheory.FLT.Three Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.InnerProductSpace.Positive Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.Topology.ContinuousMap.Units Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Kernel.Invariance Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Probability.Distributions.Uniform Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Basic Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.NumberTheory.Liouville.Measure Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Geometry.Euclidean.MongePoint Mathlib.Topology.CWComplex Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.Ostrowski Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.MeasureTheory.Measure.Doubling Mathlib.Analysis.MeanInequalities Mathlib.Probability.Distributions.Poisson Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.Analysis.InnerProductSpace.Projection Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Topology.ContinuousMap.Sigma Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.Quaternion Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.Analytic.Meromorphic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Convex.Normed Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Analysis.Convex.Continuous Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Analysis.Calculus.Darboux Mathlib.MeasureTheory.Function.Jacobian Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.MeasureTheory.Function.LpOrder Mathlib.Analysis.Convex.Measure Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Probability.Moments Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.Normed.Operator.Banach Mathlib.Algebra.Module.CharacterModule Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Convex.Contractible Mathlib.AlgebraicGeometry.AffineScheme Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.NumberTheory.Liouville.Basic Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Topology.Connected.PathConnected Mathlib.Analysis.Normed.Operator.WeakOperatorTopology Mathlib.AlgebraicGeometry.Limits Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Topology.Algebra.PontryaginDual Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Analysis.Analytic.Constructions Mathlib.Topology.MetricSpace.Holder Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Probability.Process.Stopping Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Condensed.Light.Limits Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.Topology.VectorBundle.Constructions Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.Analytic.Composition Mathlib.Topology.VectorBundle.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.ConstantSpeed Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.Calculus.Implicit Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Geometry.Manifold.IntegralCurve Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.Probability.Kernel.MeasureCompProd Mathlib.Analysis.NormedSpace.Extend Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Tactic.FunProp.Differentiable Mathlib.Probability.Independence.Integrable Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Analysis.Convolution Mathlib.AlgebraicGeometry.Scheme Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.Analytic.Uniqueness Mathlib.Condensed.Light.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.AlgebraicGeometry.Gluing Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Analysis.MellinInversion Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Dynamics.Ergodic.Function Mathlib.Topology.Separation.NotNormal Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.MeasureTheory.Covering.Differentiation Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Algebra.Order.CompleteField Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.NumberTheory.WellApproximable Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Process.Adapted Mathlib.Probability.Distributions.Pareto Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.Probability.Process.Filtration Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.LSeries.Linearity Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Probability.Kernel.Condexp Mathlib.Topology.ContinuousMap.Algebra Mathlib.Condensed.Light.Functors Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.MeasureTheory.Function.AEEqFun Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.NumberTheory.Liouville.Residual Mathlib.Analysis.Analytic.Inverse Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.Restrict Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Probability.Density Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Analysis.Calculus.Dslope Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Topology.Homotopy.Equiv Mathlib.Analysis.NormedSpace.Connected Mathlib.Topology.Homotopy.HSpaces Mathlib.Analysis.ODE.PicardLindelof Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Probability.ConditionalExpectation Mathlib.Analysis.Calculus.LogDeriv Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.MeasureTheory.Group.Integral Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Topology.Sheaves.Sheafify Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.RingTheory.Unramified.Finite Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.NumberTheory.Bertrand Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Geometry.Manifold.Metrizable Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Topology.ContinuousMap.Ideals Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.RingTheory.Perfection Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.Probability.CDF Mathlib.Analysis.Normed.Module.Completion Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Probability.Martingale.Centering Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Topology.Algebra.ContinuousMonoidHom	2
Mathlib.Topology.Hom.ContinuousEvalConst	564
Mathlib.Topology.Hom.ContinuousEval	566

---

Declarations diff

+ Continuous.coeFun
+ Continuous.eval
+ Continuous.eval_const
+ ContinuousAt.coeFun
+ ContinuousAt.eval
+ ContinuousAt.eval_const
+ ContinuousEval
+ ContinuousEval.of_continuous_forget
+ ContinuousEvalConst
+ ContinuousEvalConst.of_continuous_forget
+ ContinuousMultilinearMap.instContinuousEval
+ ContinuousOn.coeFun
+ ContinuousOn.eval
+ ContinuousOn.eval_const
+ ContinuousWithinAt.coeFun
+ ContinuousWithinAt.eval
+ ContinuousWithinAt.eval_const
+ Filter.Tendsto.coeFun
+ Filter.Tendsto.eval
+ Filter.Tendsto.eval_const
+ continuousEvalConst
+ continuous_coeFun
+ hasProd_apply
+ instT2Space
+ instance (priority := 100) ContinuousEval.toContinuousEvalConst : ContinuousEvalConst F X Y
+ instance (priority := 100) ContinuousEval.toContinuousMapClass : ContinuousMapClass F X Y
+ instance : ContinuousEval (Path x y) I X := .of_continuous_forget continuous_induced_dom
+ instance : ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F
+ instance : ContinuousEvalConst C(X, Y) X Y
+ instance [LocallyCompactPair X Y] : ContinuousEval C(X, Y) X Y
+ instance [R0Space R] : R0Space C(X, R)₀ := embedding_toContinuousMap.r0Space
+ instance [R1Space R] : R1Space C(X, R)₀ := embedding_toContinuousMap.r1Space
+ instance [RegularSpace R] : RegularSpace C(X, R)₀ := embedding_toContinuousMap.regularSpace
+ instance [T3Space R] : T3Space C(X, R)₀ := embedding_toContinuousMap.t3Space
+ multipliable_apply
+ tprod_apply
++ instTopologicalAddGroup
+++ instContinuousEval
+++++ instContinuousEvalConst
+++--- continuous_eval_const
++-- continuous_coe_fun
++-- continuous_eval
- hasSum_apply
- instance [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [T2Space F] :
- summable_apply
- tsum_apply
-++ instT3Space

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.

[ADedecker]

Thanks a lot!

Why did you put one of the new files under ContinuousMap but not the other ?

[urkud]

Why did you put one of the new files under ContinuousMap but not the other ?

I don't know. ContinuousEval is a generalization of ContinuousMapClass, but probably this isn't a good argument. Should we put both of them in Topology/? Somewhere else?

[ADedecker]

Why did you put one of the new files under ContinuousMap but not the other ?

I don't know. ContinuousEval is a generalization of ContinuousMapClass, but probably this isn't a good argument. Should we put both of them in Topology/? Somewhere else?

Ah, I see the reasoning, but I would still prefer to have them in the same folder. I think I would put them both under either Topology/ or Topology/Hom/, but feel free to keep the current situation if you want.