feat(Order): SupClosed/DirSupClosed/DirectedOn/etc for set intervals - #43536
Open
SnirBroshi wants to merge 3 commits into
Open
feat(Order): SupClosed/DirSupClosed/DirectedOn/etc for set intervals#43536SnirBroshi wants to merge 3 commits into
SupClosed/DirSupClosed/DirectedOn/etc for set intervals#43536SnirBroshi wants to merge 3 commits into
Conversation
SnirBroshi
commented
Sep 7, 2026
SnirBroshi
commented
Collaborator
PR summary d6b49f4b2e
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Order.SupClosed | 680 | 686 | +6 (+0.88%) |
| Mathlib.Order.CountableSupClosed | 700 | 706 | +6 (+0.86%) |
Import changes for all files
| Files | Import difference |
|---|---|
542 filesMathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Spectrum.Basic Mathlib.Algebra.Algebra.Spectrum.Pi Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.StrictPositivity Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.Lattice Mathlib.Algebra.Algebra.Subalgebra.Matrix Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Azumaya.Defs Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.FilteredColimits Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.End Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.Subring Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.DualNumber Mathlib.Algebra.Exact.Basic Mathlib.Algebra.Exact Mathlib.Algebra.FiveLemma Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.Injective Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Algebra.MonoidAlgebra.Module Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Coeff Mathlib.Algebra.MvPolynomial.Comap Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Division Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Defs Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.Polynomial.Module.TensorProduct Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Polynomial.OfFn Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.RingQuot Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.SkewMonoidAlgebra.Lift Mathlib.Algebra.SkewMonoidAlgebra.Single Mathlib.Algebra.SkewMonoidAlgebra.Support Mathlib.Algebra.SkewPolynomial.Basic Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.RingQuot Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Star.TensorProduct Mathlib.Algebra.Star.UnitaryStarAlgAut Mathlib.Algebra.Star.Unitary Mathlib.Algebra.TrivSqZeroExt.Basic Mathlib.Algebra.TrivSqZeroExt.Ideal Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.NNReal Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.StoneSeparation Mathlib.Analysis.Normed.Lp.WithLp Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.Reflection Mathlib.Data.Nat.Choose.Vandermonde Mathlib.FieldTheory.IntermediateField.Adjoin.Defs Mathlib.FieldTheory.IntermediateField.Basic Mathlib.FieldTheory.IsRealClosed.Basic Mathlib.FieldTheory.RatFunc.Defs Mathlib.Geometry.Convex.Cone.Basic Mathlib.Geometry.Convex.Cone.DualFinite Mathlib.Geometry.Convex.Cone.Dual Mathlib.Geometry.Convex.Cone.Face.Basic Mathlib.Geometry.Convex.Cone.Face.Lattice Mathlib.Geometry.Convex.Cone.Pointed Mathlib.Geometry.Convex.Cone.Simplicial Mathlib.Geometry.Convex.ConvexSpace.AffineSpace Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Centroid Mathlib.LinearAlgebra.AffineSpace.Ceva Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.Homogenization Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.Curry Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv Mathlib.LinearAlgebra.Complex.Module Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.DirectSum.Finite Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FixedSubmodule Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.LeftExact Mathlib.LinearAlgebra.LinearIndependent.BaseChange Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.Bilinear Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.ConjTranspose Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.DualNumber Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.Hadamard Mathlib.LinearAlgebra.Matrix.Invertible Mathlib.LinearAlgebra.Matrix.Module Mathlib.LinearAlgebra.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.RowCol Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Unique Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.DirectSum Mathlib.LinearAlgebra.Multilinear.Finsupp Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct.Basic Mathlib.LinearAlgebra.PiTensorProduct.Basis Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp Mathlib.LinearAlgebra.PiTensorProduct.DirectSum Mathlib.LinearAlgebra.PiTensorProduct.Finsupp Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Bilinear Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SModEq.Basic Mathlib.LinearAlgebra.SModEq.Pointwise Mathlib.LinearAlgebra.SModEq.Pow Mathlib.LinearAlgebra.SesquilinearForm.Basic Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.SymmetricAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorPower.Symmetric Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.Decomposition Mathlib.LinearAlgebra.TensorProduct.Defs Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.LinearAlgebra.TensorProduct.Free Mathlib.LinearAlgebra.TensorProduct.Map Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Quotient Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.MeasureTheory.Constructions.SimpleGraph Mathlib.MeasureTheory.Constructions.SubmoduleQuotient Mathlib.MeasureTheory.MeasurableSpace.Constructions Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated Mathlib.MeasureTheory.MeasurableSpace.Pi Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict Mathlib.MeasureTheory.MeasurableSpace.Prod Mathlib.MeasureTheory.SetAlgebra Mathlib.MeasureTheory.SetSemiring Mathlib.NumberTheory.Basic Mathlib.NumberTheory.Dioph Mathlib.NumberTheory.FLT.Basic Mathlib.NumberTheory.Multiplicity Mathlib.NumberTheory.PellMatiyasevic Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.Order.BooleanGenerators Mathlib.Order.CompactlyGenerated.Basic Mathlib.Order.CompactlyGenerated.Intervals Mathlib.Probability.Kernel.IonescuTulcea.Maps Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.Adjoin.Polynomial.Basic Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.Adjoin.Singleton Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.Bezout Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Convolution Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.Primitive Mathlib.RingTheory.Bialgebra.SymmetricAlgebra Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.CoassocSimps Mathlib.RingTheory.Coalgebra.Convolution Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.MonoidAlgebra Mathlib.RingTheory.Coalgebra.MulOpposite Mathlib.RingTheory.Coalgebra.Primitive Mathlib.RingTheory.Coalgebra.Quotient Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.Congruence.Hom Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.DividedPowerAlgebra.Init Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DividedPowers.DPMorphism Mathlib.RingTheory.DividedPowers.RatAlgebra Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Finiteness.Ideal Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Finiteness.Nakayama Mathlib.RingTheory.Finiteness.Nilpotent Mathlib.RingTheory.Finiteness.Prod Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.FreeRing Mathlib.RingTheory.GradedAlgebra.AlgHom Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.GradedAlgebra.RingHom Mathlib.RingTheory.GradedAlgebra.TensorProduct Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.HopfAlgebra.Convolution Mathlib.RingTheory.HopfAlgebra.Primitive Mathlib.RingTheory.HopfAlgebra.TensorProduct Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Ideal.Basis Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.Finsupp Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.RingTheory.Ideal.IsAugmentation Mathlib.RingTheory.Ideal.IsPrimary Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Oka Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Ideal.Quotient.PowTransition Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IsGaloisGroup.Defs Mathlib.RingTheory.IsPrimary Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.Jacobson.Radical Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.Localization.Rat Mathlib.RingTheory.Localization.Saturation Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.Ideal Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Noetherian.OfPrime Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.ShiftedLegendre Mathlib.RingTheory.Polynomial.Subring Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Catalan Mathlib.RingTheory.PowerSeries.CoeffMulMem Mathlib.RingTheory.PowerSeries.NoZeroDivisors Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.Schroder Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.PrincipalIdealDomainOfPrime Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.Radical.NatInt Mathlib.RingTheory.Radical Mathlib.RingTheory.SimpleRing.Principal Mathlib.RingTheory.Spectrum.Maximal.Basic Mathlib.RingTheory.Spectrum.Maximal.Defs Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.IsBaseChangeFree Mathlib.RingTheory.TensorProduct.IsBaseChangePi Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact Mathlib.RingTheory.TensorProduct.Maps Mathlib.RingTheory.TensorProduct.MonoidAlgebra Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.ValuationRing Mathlib.RingTheory.Valuation.ValuativeRel.Basic Mathlib.RingTheory.Valuation.ValuativeRel.Trivial Mathlib.Tactic.Algebraize Mathlib.Tactic.ComputeDegree Mathlib.Tactic.Echelon.Parsing Mathlib.Tactic.Echelon.Zsqrtd Mathlib.Tactic.ModuleNF Mathlib.Tactic.Module Mathlib.Tactic.Polynomial.Basic Mathlib.Tactic.Ring.NamePolyVars Mathlib.Tactic.Ring.NamePowerVars |
1 |
10 filesMathlib.Algebra.Module.Submodule.Invariant Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.Order.BooleanSubalgebra Mathlib.Order.CompleteLattice.SetLike Mathlib.Order.CompleteSublattice Mathlib.Order.CountableSupClosed Mathlib.Order.Sublattice Mathlib.Order.Sublocale Mathlib.Order.SupClosed Mathlib.SetTheory.Descriptive.Tree |
6 |
Declarations diff (regex)
+ ClosedIciTopology.of_isLowerSet
+ ClosedIicTopology.of_isLowerSet
+ CountableSupClosed.Icc
+ CountableSupClosed.Ici
+ CountableSupClosed.Iic
+ CountableSupClosed.Ioc
+ CountableSupClosed.Ioi
+ DirSupClosed.Icc
+ DirSupClosed.Ici
+ DirSupClosed.Iic
+ DirSupClosed.Ioc
+ DirSupClosed.Ioi
+ DirSupClosedOn.Icc
+ DirSupClosedOn.Ici
+ DirSupClosedOn.Iic
+ DirSupClosedOn.Ioc
+ DirSupClosedOn.Ioi
+ DirSupInacc.Iic
+ DirSupInacc.Iio
+ DirSupInacc.Ioc
+ DirSupInacc.Ioi
+ DirSupInacc.Ioo
+ DirSupInaccOn.Iic
+ DirSupInaccOn.Iio
+ DirSupInaccOn.Ioc
+ DirSupInaccOn.Ioi
+ DirSupInaccOn.Ioo
+ DirectedOn.le_Icc
+ DirectedOn.le_Ici
+ DirectedOn.le_Iic
+ DirectedOn.le_Ioc
+ DirectedOn.le_Ioi
+ IsClosed.Icc
+ IsClosed.Icc_of_isLowerSet
+ IsClosed.Ici_of_isLowerSet
+ IsClosed.Iic_of_isLowerSet
+ IsClosed.Iio
+ IsClosed.Ioc
+ IsClosed.Ioc_of_isLowerSet
+ IsClosed.Ioi_of_isLowerSet
+ IsOpen.Ici
+ IsOpen.Iic_of_isLowerSet
+ IsOpen.Iio_of_isLowerSet
+ IsOpen.Ioc
+ IsOpen.Ioc_of_isLowerSet
+ IsOpen.Ioi_of_isLowerSet
+ IsOpen.Ioo
+ IsOpen.Ioo_of_isLowerSet
+ IsUpperSet.countableSupClosed
+ SupClosed.Icc
+ SupClosed.Ici
+ SupClosed.Iic
+ SupClosed.Ioc
+ SupClosed.Ioi
+ instance : ClosedIciTopology α
+ instance : ClosedIicTopology α
+ isClosed_iff_isLowerSet
+ isClosed_iff_isUpperSet
++ IsClosed.Ici
++ IsClosed.Iic
++ IsClosed.Ioi
++ IsOpen.Iic
++ IsOpen.Iio
++ IsOpen.Ioi
- directedOn_ge_Icc
- directedOn_ge_Ici
- directedOn_ge_Ico
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
d6b49f4).
- +86 new declarations
- −0 removed declarations
+CountableInfClosed.Icc
+CountableInfClosed.Ici
+CountableInfClosed.Ico
+CountableInfClosed.Iic
+CountableInfClosed.Iio
+CountableSupClosed.Icc
+CountableSupClosed.Ici
+CountableSupClosed.Iic
+CountableSupClosed.Ioc
+CountableSupClosed.Ioi
+DirSupClosed.Icc
+DirSupClosed.Ici
+DirSupClosed.Iic
+DirSupClosed.Ioc
+DirSupClosed.Ioi
+DirSupClosedOn.Icc
+DirSupClosedOn.Ici
+DirSupClosedOn.Iic
+DirSupClosedOn.Ioc
+DirSupClosedOn.Ioi
+DirSupInacc.Iic
+DirSupInacc.Iio
+DirSupInacc.Ioc
+DirSupInacc.Ioi
+DirSupInacc.Ioo
+DirSupInaccOn.Iic
+DirSupInaccOn.Iio
+DirSupInaccOn.Ioc
+DirSupInaccOn.Ioi
+DirSupInaccOn.Ioo
+DirectedOn.ge_Icc
+DirectedOn.ge_Ici
+DirectedOn.ge_Ico
+DirectedOn.ge_Iic
+DirectedOn.ge_Iio
+DirectedOn.le_Icc
+DirectedOn.le_Ici
+DirectedOn.le_Iic
+DirectedOn.le_Ioc
+DirectedOn.le_Ioi
+InfClosed.Icc
+InfClosed.Ici
+InfClosed.Ico
+InfClosed.Iic
+InfClosed.Iio
+IsLowerSet.countableInfClosed
+IsUpperSet.countableSupClosed
+SupClosed.Icc
+SupClosed.Ici
+SupClosed.Iic
+SupClosed.Ioc
+SupClosed.Ioi
+Topology.IsLowerSet.IsClosed.Ici
+Topology.IsLowerSet.IsClosed.Ioi
+Topology.IsLowerSet.IsOpen.Iic
+Topology.IsLowerSet.IsOpen.Iio
+Topology.IsLowerSet.isClosed_iff_isUpperSet
+Topology.IsScottHausdorff.ClosedIciTopology.of_isLowerSet
+Topology.IsScottHausdorff.ClosedIicTopology.of_isLowerSet
+Topology.IsScottHausdorff.IsClosed.Icc
+Topology.IsScottHausdorff.IsClosed.Icc_of_isLowerSet
+Topology.IsScottHausdorff.IsClosed.Ici
+Topology.IsScottHausdorff.IsClosed.Ici_of_isLowerSet
+Topology.IsScottHausdorff.IsClosed.Iic
+Topology.IsScottHausdorff.IsClosed.Iic_of_isLowerSet
+Topology.IsScottHausdorff.IsClosed.Ioc
+Topology.IsScottHausdorff.IsClosed.Ioc_of_isLowerSet
+Topology.IsScottHausdorff.IsClosed.Ioi
+Topology.IsScottHausdorff.IsClosed.Ioi_of_isLowerSet
+Topology.IsScottHausdorff.IsOpen.Iic
+Topology.IsScottHausdorff.IsOpen.Iic_of_isLowerSet
+Topology.IsScottHausdorff.IsOpen.Iio
+Topology.IsScottHausdorff.IsOpen.Iio_of_isLowerSet
+Topology.IsScottHausdorff.IsOpen.Ioc
+Topology.IsScottHausdorff.IsOpen.Ioc_of_isLowerSet
+Topology.IsScottHausdorff.IsOpen.Ioi
+Topology.IsScottHausdorff.IsOpen.Ioi_of_isLowerSet
+Topology.IsScottHausdorff.IsOpen.Ioo
+Topology.IsScottHausdorff.IsOpen.Ioo_of_isLowerSet
+Topology.IsScottHausdorff.instClosedIciTopology
+Topology.IsScottHausdorff.instClosedIicTopology
+Topology.IsUpperSet.IsClosed.Iic
+Topology.IsUpperSet.IsClosed.Iio
+Topology.IsUpperSet.IsOpen.Ici
+Topology.IsUpperSet.IsOpen.Ioi
+Topology.IsUpperSet.isClosed_iff_isLowerSetNo changes to strong technical debt.
No changes to weak technical debt.
Current commit d6b49f4b2e
Reference commit 0383a80e64
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).
github-actions
Bot
added
the
t-topology
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
1 participant
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.