feat(Order/Disjointed): allow arbitrary partial orders as domain

[loefflerd]

---

• depends on: feat(Order/PartialSups): allow general orders as domain #20137

[github-actions]

PR summary 187d80b01d

Import changes exceeding 2%

%	File
+4.29%	Mathlib.LinearAlgebra.Prod
+15.05%	Mathlib.MeasureTheory.SetSemiring
+16.43%	Mathlib.Order.Disjointed
+4.22%	Mathlib.Order.PartialSups

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Disjointed	499	581	+82 (+16.43%)
Mathlib.MeasureTheory.SetSemiring	545	627	+82 (+15.05%)
Mathlib.LinearAlgebra.Prod	746	778	+32 (+4.29%)
Mathlib.Order.PartialSups	498	519	+21 (+4.22%)
Mathlib.Order.Interval.Finset.Box	652	661	+9 (+1.38%)
Mathlib.Topology.Order.PartialSups	637	644	+7 (+1.10%)

Import changes for all files

Files	Import difference
4 files Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.MeasureTheory.OuterMeasure.BorelCantelli	1
10 files Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.LinearAlgebra.Dimension.Basic Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.Algebra.Colimit.Module Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors	2
8 files Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.Analysis.LocallyConvex.Polar Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Affine Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Normed.Group.AddTorsor	3
144 files Mathlib.Algebra.Star.Module Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.AlgebraTower Mathlib.Data.Matrix.Auto Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.Algebra.Module.Bimodule Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.Data.Matrix.Invertible Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Basic Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.RingTheory.Localization.BaseChange Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.Star.Subalgebra Mathlib.GroupTheory.Coxeter.Basic Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Analysis.Convex.Slope Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.Algebra.DirectSum.Internal Mathlib.Data.Matrix.Block Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.RingTheory.DividedPowers.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.RingTheory.PolynomialAlgebra Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.Algebra.Algebra.Unitization Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.Algebra.DirectSum.Decomposition Mathlib.RingTheory.Polynomial.Bernstein Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.Analysis.Convex.Cone.Extension Mathlib.Algebra.MvPolynomial.Rename Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.Data.Matrix.Reflection Mathlib.Algebra.Module.Projective Mathlib.Analysis.Convex.Join Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.Algebra.MvPolynomial.Derivation Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Algebra.CharP.Subring Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.MvPolynomial.Supported Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Algebra.DirectSum.Finsupp Mathlib.LinearAlgebra.LinearIndependent Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.Algebra.Algebra.Spectrum Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.MvPolynomial.Comap Mathlib.RingTheory.Polynomial.Wronskian Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.LinearAlgebra.Ray Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Segment Mathlib.RingTheory.Adjoin.Polynomial Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Algebra.Star.Free Mathlib.Algebra.MvPolynomial.Monad Mathlib.LinearAlgebra.Alternating.Basic Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Analysis.Convex.Function Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.RingTheory.MatrixAlgebra Mathlib.Analysis.Convex.Cone.Basic Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.Algebra.MvPolynomial.Division Mathlib.Data.Complex.Module Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.RingTheory.TensorProduct.Pi Mathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Star Mathlib.LinearAlgebra.Basis.Basic Mathlib.Analysis.Convex.Basic Mathlib.Algebra.CharP.Algebra Mathlib.RingTheory.Localization.Module Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Data.Matrix.RowCol Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Analysis.Convex.Extreme Mathlib.LinearAlgebra.TensorPower Mathlib.Data.Matrix.Hadamard Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.Algebra.CharP.IntermediateField Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.Analysis.Convex.Quasiconvex Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Algebra.DirectSum.Algebra Mathlib.RingTheory.TensorProduct.Free Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Data.Matrix.ConjTranspose Mathlib.Algebra.Star.Unitary Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.Data.Matrix.Notation Mathlib.RingTheory.TensorProduct.Basic Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.Algebra.Module.GradedModule Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Algebra.FreeAlgebra Mathlib.RingTheory.PowerSeries.Trunc Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.FieldTheory.Differential.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.LinearAlgebra.FreeProduct.Basic	4
Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.MeasureTheory.MeasurableSpace.Card	5
Mathlib.Topology.Order.PartialSups	7
Mathlib.Order.Interval.Finset.Box	9
Mathlib.MeasureTheory.Measure.AddContent	11
3 files Mathlib.Algebra.TrivSqZeroExt Mathlib.Data.Matrix.DualNumber Mathlib.Algebra.DualNumber	18
Mathlib.Order.PartialSups	21
4 files Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.Algebra.Module.Injective Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Prod	32
Mathlib.MeasureTheory.Constructions.SubmoduleQuotient	33
Mathlib.MeasureTheory.Constructions.AddChar	39
Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict	40
6 files Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.MeasureTheory.MeasurableSpace.Pi Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.MeasureTheory.MeasurableSpace.Prod Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated	42
Mathlib.MeasureTheory.MeasurableSpace.Instances	68
7 files Mathlib.Order.Disjointed Mathlib.MeasureTheory.MeasurableSpace.Defs Mathlib.MeasureTheory.SetAlgebra Mathlib.MeasureTheory.MeasurableSpace.Invariants Mathlib.MeasureTheory.PiSystem Mathlib.MeasureTheory.SetSemiring Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable	82

---

Declarations diff

+ Fintype.exists_disjointed_le
+ Fintype.sup_disjointed
+ Monotone.disjointed_add_one
+ Monotone.disjointed_add_one_sup
+ Nat.disjointedRec
+ Pi.partialSups_apply
+ ciSup_partialSups_eq'
+ disjoint_disjointed_of_lt
+ disjointed_add_one
+ disjointed_apply
+ disjointed_bot
+ disjointed_eq_self
+ disjointed_of_isMin
+ disjointed_partialSups
+ disjointed_unique'
+ partialSups_add_one
+ partialSups_bot
+ sup_mem

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(Order/PartialSups): allow general orders as domain #20137
  By Dependent Issues (🤖). Happy coding!