feat: generalize normal functions

[vihdzp]

In ordinal/cardinal arithmetic, a normal function is a strictly monotonic continuous function. Unfortunately, defining normal functions like this would add hundreds of imports to the respective files, so we opt for a definition that's more lightweight and more convenient: a normal function is a strictly monotonic function where, for a successor limit a, the value f a is the LUB of f b for b < a.

The predicate Ordinal.IsNormal already exists. This generalization serves two purposes:

1. We can now talk about normality of functions between ordinals and cardinals, rather than functions that are strictly between ordinals. Examples include Cardinal.ord, Cardinal.aleph, and Cardinal.beth.
2. This is also useful to my project on formalizing ordinal notations, as I can now state that addition, multiplication, etc. defined on an ordinal notation are also normal functions.

A future PR will deprecate Ordinal.IsNormal in favor of this new predicate.

---

• depends on: feat: IsSuccPrelimit a → IsLUB (Iio a) a #20496
• depends on: feat: generalize IsLUB.mem_of_not_isSuccPrelimit to LinearOrder #20502
• depends on: [Merged by Bors] - feat: initial segment commutes with Iio #20503

[github-actions]

PR summary fd1844f890

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.UpperLower.Basic	369	375	+6 (+1.63%)

Import changes for all files

Files	Import difference
632 files Mathlib.Topology.Algebra.Monoid Mathlib.Algebra.Star.Module Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Topology.Order.LawsonTopology Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.Topology.Instances.Nat Mathlib.CategoryTheory.Sites.Pullback Mathlib.Topology.Algebra.Semigroup Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.Topology.CompactOpen Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.RingTheory.Ideal.Span Mathlib.LinearAlgebra.Span.Basic Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.RingTheory.AlgebraTower Mathlib.Data.Matrix.Auto Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.Topology.IndicatorConstPointwise Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Topology.ContinuousMap.Ordered Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Analysis.Polynomial.CauchyBound Mathlib.RingTheory.Polynomial.Ideal Mathlib.NumberTheory.Multiplicity Mathlib.Topology.DerivedSet Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.Topology.Algebra.UniformField Mathlib.Algebra.Module.Bimodule Mathlib.CategoryTheory.Action.Continuous Mathlib.Topology.DiscreteSubset Mathlib.Topology.Compactification.OnePoint Mathlib.Topology.Instances.PNat Mathlib.Topology.DenseEmbedding Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.Topology.UniformSpace.OfCompactT2 Mathlib.Topology.Algebra.UniformGroup.Basic Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.UniformSpace.Compact Mathlib.Topology.Order.Lattice Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.Data.Matrix.Invertible Mathlib.Topology.Instances.Int Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.RingTheory.Ideal.Maps Mathlib.Algebra.DirectSum.Module Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.FiberBundle.Constructions Mathlib.Combinatorics.Hall.Basic Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.Topology.Sets.Closeds Mathlib.Algebra.MvPolynomial.Counit Mathlib.Topology.Order.ScottTopology Mathlib.Algebra.MvPolynomial.Basic Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.Topology.Order.OrderClosedExtr Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.RingTheory.Algebraic.Defs Mathlib.LinearAlgebra.DFinsupp Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.Topology.Compactness.LocallyCompact Mathlib.Algebra.RingQuot Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Topology.Order.Compact Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.ShrinkingLemma Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.RingTheory.Localization.BaseChange Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.Topology.Order.ExtendFrom Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Dynamics.OmegaLimit Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.RingTheory.Polynomial.Tower Mathlib.CategoryTheory.Sites.EpiMono Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicTopology.CechNerve Mathlib.Order.Filter.FilterProduct Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Order.Filter.Ultrafilter Mathlib.Topology.Filter Mathlib.Topology.Order.PartialSups Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.Topology.Sheaves.Forget Mathlib.Algebra.MvPolynomial.Expand Mathlib.Order.Filter.Subsingleton Mathlib.Analysis.Oscillation Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Star.Subalgebra Mathlib.Topology.LocalAtTarget Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.Order.ProjIcc Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Lipschitz Mathlib.GroupTheory.Coxeter.Basic Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.Topology.Instances.Discrete Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.Topology.Spectral.Hom Mathlib.Algebra.Central.Defs Mathlib.Topology.PartialHomeomorph Mathlib.Topology.ClopenBox Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Algebra.Vertex.HVertexOperator Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Topology.Sequences Mathlib.Analysis.Convex.Slope Mathlib.Topology.Order.Monotone Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Algebra.WithZeroTopology Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Localization.Away.Basic Mathlib.Topology.Algebra.Order.Field Mathlib.Algebra.Polynomial.RingDivision Mathlib.Analysis.Normed.Field.Basic Mathlib.Algebra.Algebra.Operations Mathlib.Topology.Order.LowerUpperTopology Mathlib.Order.Filter.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.Algebra.Polynomial.Taylor Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Maps.Proper.Basic Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.Order.CompactlyGenerated.Intervals Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Topology.Sober Mathlib.Topology.ExtendFrom Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.RingTheory.Coprime.Ideal Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.Topology.MetricSpace.ProperSpace Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.Topology.Order.Filter Mathlib.Algebra.DirectSum.Internal Mathlib.Data.Matrix.Block Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.Topology.Algebra.Star Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.Topology.Separation.CountableSeparatingOn Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.DividedPowers.Basic Mathlib.Topology.ContinuousMap.SecondCountableSpace Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Topology.Order.Basic Mathlib.Topology.Algebra.Equicontinuity Mathlib.RingTheory.PiTensorProduct Mathlib.Topology.Instances.ENat Mathlib.Topology.Homeomorph Mathlib.Topology.ContinuousMap.Basic Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Topology.List Mathlib.RingTheory.LocalRing.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Topology.Algebra.UniformGroup.Defs Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.RingTheory.PolynomialAlgebra Mathlib.Topology.ContinuousMap.CocompactMap Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Topology.Algebra.UniformMulAction Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.Algebra.Algebra.Unitization Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.Topology.Gluing Mathlib.Algebra.DirectSum.Decomposition Mathlib.Topology.Connected.LocallyConnected Mathlib.RingTheory.Polynomial.Bernstein Mathlib.Topology.Sets.Order Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Topology.UniformSpace.Matrix Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Topology.MetricSpace.Isometry Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.Algebra.MvPolynomial.Rename Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.Data.Matrix.Reflection Mathlib.Algebra.Module.Projective Mathlib.Topology.Hom.Open Mathlib.Topology.Algebra.MulAction Mathlib.LinearAlgebra.Basis.Defs Mathlib.Analysis.Convex.Join Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Order.Floor.Prime Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.Algebra.MvPolynomial.Derivation Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Algebra.CharP.Subring Mathlib.Algebra.MvPolynomial.Variables Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.Order.NhdsSet Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Algebra.MvPolynomial.Supported Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Geometry.RingedSpace.Basic Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Order.LeftRightLim Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Algebra.DirectSum.Finsupp Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.LinearAlgebra.LinearIndependent Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.Topology.FiberPartition Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Topology.Connected.Clopen Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.Algebra.Algebra.Spectrum Mathlib.Topology.Order.MonotoneConvergence Mathlib.RingTheory.Binomial Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Topology.Algebra.MvPolynomial Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.Analysis.NormedSpace.MStructure Mathlib.Topology.ContinuousMap.Sigma Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Order.Rolle Mathlib.Topology.Algebra.ConstMulAction Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Topology.NoetherianSpace Mathlib.Topology.Algebra.Field Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.LinearAlgebra.Matrix.Trace Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.LinearAlgebra.SesquilinearForm Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Topology.Category.TopCat.Opens Mathlib.Algebra.Star.RingQuot Mathlib.CategoryTheory.CofilteredSystem Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.MvPolynomial.Comap Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Topology.Covering Mathlib.RingTheory.Polynomial.Wronskian Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.CategoryTheory.Sites.Spaces Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.Topology.Metrizable.Basic Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.FiberBundle.Trivialization Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Sheaves.Limits Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.Data.Matrix.Bilinear Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.LinearAlgebra.Ray Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Convex.Mul Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.StoneCech Mathlib.Analysis.Convex.Segment Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.Algebra.Module.Injective Mathlib.Topology.FiberBundle.Basic Mathlib.Topology.Separation.Profinite Mathlib.RingTheory.Algebraic.Pi Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.ContinuousMap.Interval Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.JacobsonSpace Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.Topology.Specialization Mathlib.Topology.Connected.Basic Mathlib.Topology.Sheaves.LocallySurjective Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.Topology.Irreducible Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.RingTheory.HahnSeries.Valuation Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.RingTheory.Adjoin.Polynomial Mathlib.CategoryTheory.Sites.Equivalence Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.Topology.Algebra.Constructions Mathlib.Topology.UniformSpace.Cauchy Mathlib.RingTheory.Valuation.Integers Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.AlgebraicTopology.SimplexCategory Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.Order.DenselyOrdered Mathlib.RingTheory.HahnSeries.Summable Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Topology.UniformSpace.Separation Mathlib.Topology.Compactness.Lindelof Mathlib.Algebra.Star.Free Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.Topology.Algebra.Affine Mathlib.RingTheory.Localization.Basic Mathlib.Algebra.MvPolynomial.Monad Mathlib.RingTheory.Ideal.Operations Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.FilterBasis Mathlib.LinearAlgebra.Alternating.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.Algebra.Colimit.Module Mathlib.RingTheory.Localization.NumDen Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Topology.SeparatedMap Mathlib.Dynamics.Minimal Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Order.LeftRightNhds Mathlib.Combinatorics.Hindman Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Analysis.Convex.Function Mathlib.FieldTheory.RatFunc.Defs Mathlib.Topology.MetricSpace.Basic Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Order.BooleanGenerators Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.Topology.RestrictGen Mathlib.Topology.Separation.Hausdorff Mathlib.Topology.Order.OrderClosed Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.AlgebraicTopology.SplitSimplicialObject Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Sets.Compacts Mathlib.Topology.MetricSpace.Gluing Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.RingTheory.MvPowerSeries.Order Mathlib.Topology.UniformSpace.HeineCantor Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.Topology.Connected.TotallyDisconnected Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.RingTheory.MatrixAlgebra Mathlib.Analysis.Convex.Cone.Basic Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.RingTheory.Adjoin.Basic Mathlib.Tactic.Module Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.Dynamics.Flow Mathlib.Algebra.MvPolynomial.Division Mathlib.Topology.Separation.Basic Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Data.Complex.Module Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Topology.ApproximateUnit Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.GroupCompletion Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.RingTheory.TensorProduct.Pi Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.Topology.Category.Sequential Mathlib.Analysis.Convex.Strict Mathlib.Topology.Compactness.SigmaCompact Mathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Topology.DiscreteQuotient Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Algebra.Central.Basic Mathlib.Topology.Compactness.Compact Mathlib.RingTheory.Valuation.ValExtension Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.Topology.Sets.Opens Mathlib.Algebra.Polynomial.Lifts Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Star Mathlib.Topology.Algebra.Order.Group Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Colon Mathlib.LinearAlgebra.Basis.Basic Mathlib.Topology.Defs.Ultrafilter Mathlib.Analysis.Convex.Basic Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.InformationTheory.Hamming Mathlib.Algebra.CharP.Algebra Mathlib.RingTheory.Localization.Module Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Data.Matrix.RowCol Mathlib.RingTheory.PowerSeries.Order Mathlib.Dynamics.FixedPoints.Topology Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.Topology.Algebra.Localization Mathlib.Algebra.Algebra.Bilinear Mathlib.Data.Matrix.DualNumber Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.Topology.Order.T5 Mathlib.Topology.KrullDimension Mathlib.LinearAlgebra.TensorPower Mathlib.NumberTheory.Basic Mathlib.Topology.Order.Priestley Mathlib.CategoryTheory.Extensive Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.Topology.Perfect Mathlib.Data.Matrix.Hadamard Mathlib.Analysis.Normed.Group.Submodule Mathlib.Topology.Sheaves.PUnit Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Central.Matrix Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.Polynomial.Basis Mathlib.AlgebraicTopology.MooreComplex Mathlib.Topology.Compactness.Paracompact Mathlib.Topology.Sheaves.Presheaf Mathlib.CategoryTheory.Adhesive Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Finsupp.Span Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.Topology.Order.IntermediateValue Mathlib.Topology.Algebra.Order.Floor Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Topology.IsLocalHomeomorph Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Normed.Group.Constructions Mathlib.RingTheory.Ideal.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.RingTheory.Ideal.Basis Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Topology.Category.TopCommRingCat Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.Analysis.Convex.Quasiconvex Mathlib.Topology.OmegaCompletePartialOrder Mathlib.FieldTheory.IntermediateField.Basic Mathlib.RingTheory.Ideal.Prod Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Topology.Algebra.GroupWithZero Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Algebra.DirectSum.Algebra Mathlib.Topology.Connected.Separation Mathlib.Topology.Category.UniformSpace Mathlib.Topology.Order.ExtrClosure Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.TensorProduct.Free Mathlib.Topology.Category.FinTopCat Mathlib.Topology.Algebra.Support Mathlib.Topology.Separation.GDelta Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Topology.Algebra.Module.WeakBilin Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Data.Matrix.ConjTranspose Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.Topology.Separation.Regular Mathlib.Algebra.DualNumber Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Algebra.Star.Unitary Mathlib.Topology.Order.IsLUB Mathlib.LinearAlgebra.LinearPMap Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.Prod Mathlib.Topology.Sheaves.Sheafify Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Topology.Compactness.Exterior Mathlib.RingTheory.Valuation.Basic Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Data.Matrix.Notation Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.TensorProduct.Basic Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.Algebra.Module.GradedModule Mathlib.Topology.Order.MonotoneContinuity Mathlib.RingTheory.Valuation.RankOne Mathlib.Algebra.Algebra.Tower Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.AlexandrovDiscrete Mathlib.Tactic.Algebraize Mathlib.Topology.UniformSpace.Equiv Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.Topology.Ultrafilter Mathlib.Order.CompactlyGenerated.Basic Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Topology.Sheaves.Stalks Mathlib.Algebra.FreeAlgebra Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.Ideal.Nonunits Mathlib.Analysis.Normed.Group.Basic Mathlib.Topology.Algebra.Group.Quotient Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.Topology.Exterior Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Order.Filter.EventuallyConst Mathlib.Algebra.Polynomial.Smeval Mathlib.LinearAlgebra.StdBasis Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.Topology.Instances.Sign Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.FieldTheory.Differential.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.Topology.Inseparable Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.Topology.MetricSpace.Bounded Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.Topology.QuasiSeparated Mathlib.Topology.Algebra.Order.Archimedean	2
Mathlib.NumberTheory.MaricaSchoenheim	3
37 files Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Order.CountableDenseLinearOrder Mathlib.Algebra.Colimit.DirectLimit Mathlib.Order.PrimeIdeal Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.Order.PFilter Mathlib.Order.Ideal Mathlib.Order.ZornAtoms Mathlib.Data.Fintype.Order Mathlib.Order.Birkhoff Mathlib.Order.Zorn Mathlib.Order.PrimeSeparator Mathlib.Data.Finset.Sups Mathlib.Combinatorics.SetFamily.Kleitman Mathlib.Order.Category.FinBoolAlg Mathlib.Order.UpperLower.Basic Mathlib.Order.Category.NonemptyFinLinOrd Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Order.UpperLower.Hom Mathlib.Data.Nat.Cast.SetInterval Mathlib.Order.Category.FinBddDistLat Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Data.Set.Sups Mathlib.Combinatorics.Young.YoungDiagram Mathlib.Order.Minimal Mathlib.Algebra.Order.UpperLower Mathlib.Combinatorics.Young.SemistandardTableau Mathlib.Combinatorics.Colex Mathlib.Order.DirectedInverseSystem Mathlib.Combinatorics.SetFamily.HarrisKleitman Mathlib.Combinatorics.SetFamily.LYM Mathlib.Combinatorics.SetFamily.Intersecting Mathlib.Order.UpperLower.LocallyFinite Mathlib.SetTheory.Cardinal.SchroederBernstein Mathlib.Order.Extension.Linear Mathlib.Combinatorics.SetFamily.KruskalKatona Mathlib.Order.KrullDimension	6
Mathlib.Order.Normal (new file)	387

---

Declarations diff

+ InitialSeg.image_Iio
+ IsNormal
+ IsPredLimit.isGLB_Ioi
+ IsPredPrelimit.isGLB_Ioi
+ IsSuccLimit.isLUB_Iio
+ IsSuccPrelimit.isLUB_Iio
+ PrincipalSeg.image_Iio
+ _root_.InitialSeg.isNormal
+ _root_.IsGLB.isPredLimit_of_not_mem
+ _root_.IsGLB.isPredPrelimit_of_not_mem
+ _root_.IsLUB.isSuccLimit_of_not_mem
+ _root_.IsLUB.isSuccPrelimit_of_not_mem
+ _root_.PrincipalSeg.isNormal
+ id
+ id_le
+ inj
+ isGLB_Ioi_iff_isPredPrelimit
+ isLUB_Iio_iff_isSuccPrelimit
+ isLUB_image_Iio_of_isSuccLimit
+ le_apply
+ le_iff_forall_le
+ le_iff_le
+ lt_iff_exists_lt
+ lt_iff_lt
+ map_iSup
+ map_isLUB
+ map_sSup
+ of_succ_lt
+ trans
++ map_isSuccPrelimit
+++ map_isSuccLimit
++++ _

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: IsSuccPrelimit a → IsLUB (Iio a) a #20496
• feat: generalize IsLUB.mem_of_not_isSuccPrelimit to LinearOrder #20502
• [Merged by Bors] - feat: initial segment commutes with Iio #20503
  By Dependent Issues (🤖). Happy coding!