[Merged by Bors] - feat(Data/Finset/Sum): supremum over a disjoint union by qawbecrdtey · Pull Request #22983 · leanprover-community/mathlib4

qawbecrdtey · 2025-03-16T16:19:46Z

Add sup_disjSum and inf_disjSum.

sup_disjSum:

(s.disjSum t).sup f = (s.sup fun x ↦ f (Sum.inl x)) ⊔ (t.sup fun x ↦ f (Sum.inr x))

inf_disjSum:

(s.disjSum t).inf f = (s.inf fun x ↦ f (Sum.inl x)) ⊓ (t.inf fun x ↦ f (Sum.inr x))

github-actions · 2025-03-16T16:20:47Z

PR summary aaaef244d0

Import changes exceeding 2%

%	File
+3.42%	`Mathlib.Data.Finset.Lattice.Fold`
+3.18%	`Mathlib.Data.Finset.Max`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Finset.Lattice.Fold	438	453	+15 (+3.42%)
Mathlib.Data.Finset.Max	440	454	+14 (+3.18%)

Import changes for all files

Files	Import difference
304 files `Mathlib.Algebra.Homology.Augment` `Mathlib.Algebra.Homology.DifferentialObject` `Mathlib.Algebra.Homology.Double` `Mathlib.Algebra.Homology.Embedding.Boundary` `Mathlib.Algebra.Homology.Functor` `Mathlib.Algebra.Homology.HomologicalBicomplex` `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.Algebra.Homology.HomologicalComplex` `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.Algebra.Homology.Single` `Mathlib.Algebra.Order.Group.Finset` `Mathlib.AlgebraicTopology.CechNerve` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.SimplexCategory.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono` `Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.AlgebraicTopology.SimplicialObject.Basic` `Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialObject.Split` `Mathlib.AlgebraicTopology.SimplicialSet.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.Boundary` `Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialSet.Degenerate` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.AlgebraicTopology.SimplicialSet.Horn` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction` `Mathlib.AlgebraicTopology.SimplicialSet.Nerve` `Mathlib.AlgebraicTopology.SimplicialSet.Path` `Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex` `Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal` `Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex` `Mathlib.CategoryTheory.Action.Continuous` `Mathlib.CategoryTheory.Adhesive` `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.Category.Cat.Colimit` `Mathlib.CategoryTheory.CofilteredSystem` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.CategoryTheory.EffectiveEpi.Extensive` `Mathlib.CategoryTheory.Extensive` `Mathlib.CategoryTheory.Generator.Basic` `Mathlib.CategoryTheory.Generator.HomologicalComplex` `Mathlib.CategoryTheory.Generator.Presheaf` `Mathlib.CategoryTheory.Limits.Constructions.Filtered` `Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers` `Mathlib.CategoryTheory.Limits.Constructions.Over.Basic` `Mathlib.CategoryTheory.Limits.FintypeCat` `Mathlib.CategoryTheory.Limits.Indization.Category` `Mathlib.CategoryTheory.Limits.Lattice` `Mathlib.CategoryTheory.Limits.MorphismProperty` `Mathlib.CategoryTheory.Limits.Set` `Mathlib.CategoryTheory.Subobject.Lattice` `Mathlib.CategoryTheory.Subobject.Limits` `Mathlib.Combinatorics.Hall.Basic` `Mathlib.Combinatorics.Hall.Finite` `Mathlib.Combinatorics.SetFamily.HarrisKleitman` `Mathlib.Combinatorics.SetFamily.Kleitman` `Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp` `Mathlib.Combinatorics.SimpleGraph.Dart` `Mathlib.Combinatorics.SimpleGraph.Maps` `Mathlib.Combinatorics.SimpleGraph.Walk` `Mathlib.Data.Analysis.Filter` `Mathlib.Data.Analysis.Topology` `Mathlib.Data.Finite.Sigma` `Mathlib.Data.Finmap` `Mathlib.Data.Finset.Functor` `Mathlib.Data.Finset.Lattice.Pi` `Mathlib.Data.Finset.Lattice.Prod` `Mathlib.Data.Finset.NAry` `Mathlib.Data.Finset.PiInduction` `Mathlib.Data.Finset.Powerset` `Mathlib.Data.Finset.Sigma` `Mathlib.Data.Finset.Sym` `Mathlib.Data.Fintype.List` `Mathlib.Data.Fintype.Powerset` `Mathlib.Data.Fintype.Sigma` `Mathlib.Data.List.Cycle` `Mathlib.Data.Nat.PrimeFin` `Mathlib.Data.Set.Finite.Lattice` `Mathlib.Data.Set.Finite.Lemmas` `Mathlib.Data.Set.Finite.List` `Mathlib.Data.Set.Finite.Monad` `Mathlib.Data.Set.Finite.Powerset` `Mathlib.Data.Set.MemPartition` `Mathlib.Data.Set.Sups` `Mathlib.Data.SetLike.Fintype` `Mathlib.Dynamics.FixedPoints.Topology` `Mathlib.Dynamics.Minimal` `Mathlib.Dynamics.PeriodicPts.Defs` `Mathlib.Dynamics.PeriodicPts.Lemmas` `Mathlib.GroupTheory.GroupAction.Basic` `Mathlib.GroupTheory.GroupAction.FixedPoints` `Mathlib.GroupTheory.GroupAction.FixingSubgroup` `Mathlib.Order.BooleanSubalgebra` `Mathlib.Order.Category.FinBddDistLat` `Mathlib.Order.Category.FinBoolAlg` `Mathlib.Order.Category.NonemptyFinLinOrd` `Mathlib.Order.Category.OmegaCompletePartialOrder` `Mathlib.Order.CompleteLattice.SetLike` `Mathlib.Order.CompleteSublattice` `Mathlib.Order.ConditionallyCompleteLattice.Finset` `Mathlib.Order.Filter.AtTopBot.Archimedean` `Mathlib.Order.Filter.AtTopBot.CountablyGenerated` `Mathlib.Order.Filter.AtTopBot.Finite` `Mathlib.Order.Filter.AtTopBot.Floor` `Mathlib.Order.Filter.Bases.Finite` `Mathlib.Order.Filter.Cofinite` `Mathlib.Order.Filter.CountablyGenerated` `Mathlib.Order.Filter.EventuallyConst` `Mathlib.Order.Filter.Finite` `Mathlib.Order.Filter.Interval` `Mathlib.Order.Filter.Lift` `Mathlib.Order.Filter.Pi` `Mathlib.Order.Filter.Pointwise` `Mathlib.Order.Filter.SmallSets` `Mathlib.Order.Filter.Subsingleton` `Mathlib.Order.Filter.Ultrafilter.Basic` `Mathlib.Order.JordanHolder` `Mathlib.Order.Partition.Basic` `Mathlib.Order.RelSeries` `Mathlib.Order.Sublattice` `Mathlib.Order.SupClosed` `Mathlib.Order.SupIndep` `Mathlib.SetTheory.Descriptive.Tree` `Mathlib.Topology.AlexandrovDiscrete` `Mathlib.Topology.Algebra.ConstMulAction` `Mathlib.Topology.Algebra.Constructions.DomMulAct` `Mathlib.Topology.Algebra.Constructions` `Mathlib.Topology.Algebra.Indicator` `Mathlib.Topology.Algebra.MulAction` `Mathlib.Topology.Algebra.Order.Archimedean` `Mathlib.Topology.Algebra.Order.Support` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.Topology.Algebra.ProperConstSMul` `Mathlib.Topology.Algebra.Semigroup` `Mathlib.Topology.Algebra.Star.Real` `Mathlib.Topology.Algebra.Star` `Mathlib.Topology.Algebra.Support` `Mathlib.Topology.Baire.Lemmas` `Mathlib.Topology.Bases` `Mathlib.Topology.Basic` `Mathlib.Topology.Bornology.Absorbs` `Mathlib.Topology.Bornology.Basic` `Mathlib.Topology.Bornology.Constructions` `Mathlib.Topology.Bornology.Hom` `Mathlib.Topology.Category.Born` `Mathlib.Topology.Category.CompHausLike.Basic` `Mathlib.Topology.Category.CompHausLike.Limits` `Mathlib.Topology.Category.CompHausLike.SigmaComparison` `Mathlib.Topology.Category.FinTopCat` `Mathlib.Topology.Category.TopCat.Adjunctions` `Mathlib.Topology.Category.TopCat.Basic` `Mathlib.Topology.Category.TopCat.EffectiveEpi` `Mathlib.Topology.Category.TopCat.EpiMono` `Mathlib.Topology.Category.TopCat.Limits.Basic` `Mathlib.Topology.Category.TopCat.Limits.Cofiltered` `Mathlib.Topology.Category.TopCat.Limits.Konig` `Mathlib.Topology.Category.TopCat.Limits.Products` `Mathlib.Topology.Category.TopCat.Limits.Pullbacks` `Mathlib.Topology.Category.TopCat.ULift` `Mathlib.Topology.Category.TopCat.Yoneda` `Mathlib.Topology.Category.UniformSpace` `Mathlib.Topology.Clopen` `Mathlib.Topology.CompactOpen` `Mathlib.Topology.Compactness.Compact` `Mathlib.Topology.Compactness.Exterior` `Mathlib.Topology.Compactness.Lindelof` `Mathlib.Topology.Compactness.LocallyCompact` `Mathlib.Topology.Compactness.Paracompact` `Mathlib.Topology.Compactness.SigmaCompact` `Mathlib.Topology.Connected.Basic` `Mathlib.Topology.Connected.Clopen` `Mathlib.Topology.Connected.LocallyConnected` `Mathlib.Topology.Connected.Separation` `Mathlib.Topology.Connected.TotallyDisconnected` `Mathlib.Topology.Constructions.SumProd` `Mathlib.Topology.Constructions` `Mathlib.Topology.ContinuousMap.Basic` `Mathlib.Topology.ContinuousMap.CocompactMap` `Mathlib.Topology.ContinuousMap.Interval` `Mathlib.Topology.ContinuousMap.Ordered` `Mathlib.Topology.ContinuousMap.SecondCountableSpace` `Mathlib.Topology.ContinuousMap.Sigma` `Mathlib.Topology.ContinuousOn` `Mathlib.Topology.Defs.Induced` `Mathlib.Topology.DenseEmbedding` `Mathlib.Topology.DerivedSet` `Mathlib.Topology.DiscreteSubset` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.ExtendFrom` `Mathlib.Topology.Exterior` `Mathlib.Topology.ExtremallyDisconnected` `Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle` `Mathlib.Topology.Filter` `Mathlib.Topology.GDelta.Basic` `Mathlib.Topology.GDelta.UniformSpace` `Mathlib.Topology.Hom.ContinuousEvalConst` `Mathlib.Topology.Hom.ContinuousEval` `Mathlib.Topology.Hom.Open` `Mathlib.Topology.Homeomorph.Defs` `Mathlib.Topology.Homeomorph.Lemmas` `Mathlib.Topology.IndicatorConstPointwise` `Mathlib.Topology.Inseparable` `Mathlib.Topology.Instances.Shrink` `Mathlib.Topology.Instances.ZMod` `Mathlib.Topology.Irreducible` `Mathlib.Topology.LocallyClosed` `Mathlib.Topology.LocallyFinite` `Mathlib.Topology.Maps.Basic` `Mathlib.Topology.Maps.OpenQuotient` `Mathlib.Topology.Maps.Proper.Basic` `Mathlib.Topology.Maps.Proper.UniversallyClosed` `Mathlib.Topology.MetricSpace.Congruence` `Mathlib.Topology.MetricSpace.Defs` `Mathlib.Topology.MetricSpace.Equicontinuity` `Mathlib.Topology.MetricSpace.MetricSeparated` `Mathlib.Topology.MetricSpace.Pseudo.Constructions` `Mathlib.Topology.MetricSpace.Pseudo.Defs` `Mathlib.Topology.MetricSpace.Pseudo.Lemmas` `Mathlib.Topology.MetricSpace.Similarity` `Mathlib.Topology.MetricSpace.Ultra.Basic` `Mathlib.Topology.MetricSpace.Ultra.TotallySeparated` `Mathlib.Topology.NhdsSet` `Mathlib.Topology.OmegaCompletePartialOrder` `Mathlib.Topology.Order.Basic` `Mathlib.Topology.Order.Bornology` `Mathlib.Topology.Order.Category.AlexDisc` `Mathlib.Topology.Order.Compact` `Mathlib.Topology.Order.DenselyOrdered` `Mathlib.Topology.Order.ExtendFrom` `Mathlib.Topology.Order.ExtrClosure` `Mathlib.Topology.Order.Filter` `Mathlib.Topology.Order.Hom.Basic` `Mathlib.Topology.Order.Hom.Esakia` `Mathlib.Topology.Order.IntermediateValue` `Mathlib.Topology.Order.IsLUB` `Mathlib.Topology.Order.IsLocallyClosed` `Mathlib.Topology.Order.Lattice` `Mathlib.Topology.Order.LawsonTopology` `Mathlib.Topology.Order.LeftRightLim` `Mathlib.Topology.Order.LeftRightNhds` `Mathlib.Topology.Order.LeftRight` `Mathlib.Topology.Order.LocalExtr` `Mathlib.Topology.Order.LowerUpperTopology` `Mathlib.Topology.Order.MonotoneContinuity` `Mathlib.Topology.Order.MonotoneConvergence` `Mathlib.Topology.Order.Monotone` `Mathlib.Topology.Order.NhdsSet` `Mathlib.Topology.Order.OrderClosedExtr` `Mathlib.Topology.Order.OrderClosed` `Mathlib.Topology.Order.Priestley` `Mathlib.Topology.Order.ProjIcc` `Mathlib.Topology.Order.Rolle` `Mathlib.Topology.Order.ScottTopology` `Mathlib.Topology.Order.T5` `Mathlib.Topology.Order.UpperLowerSetTopology` `Mathlib.Topology.Order` `Mathlib.Topology.Partial` `Mathlib.Topology.Perfect` `Mathlib.Topology.Piecewise` `Mathlib.Topology.RestrictGen` `Mathlib.Topology.SeparatedMap` `Mathlib.Topology.Separation.Basic` `Mathlib.Topology.Separation.CountableSeparatingOn` `Mathlib.Topology.Separation.GDelta` `Mathlib.Topology.Separation.Hausdorff` `Mathlib.Topology.Separation.Profinite` `Mathlib.Topology.Separation.Regular` `Mathlib.Topology.Separation.SeparatedNhds` `Mathlib.Topology.Sequences` `Mathlib.Topology.ShrinkingLemma` `Mathlib.Topology.Specialization` `Mathlib.Topology.Spectral.Hom` `Mathlib.Topology.StoneCech` `Mathlib.Topology.Ultrafilter` `Mathlib.Topology.UniformSpace.AbsoluteValue` `Mathlib.Topology.UniformSpace.AbstractCompletion` `Mathlib.Topology.UniformSpace.Ascoli` `Mathlib.Topology.UniformSpace.Basic` `Mathlib.Topology.UniformSpace.Cauchy` `Mathlib.Topology.UniformSpace.CompactConvergence` `Mathlib.Topology.UniformSpace.Compact` `Mathlib.Topology.UniformSpace.CompleteSeparated` `Mathlib.Topology.UniformSpace.Completion` `Mathlib.Topology.UniformSpace.Defs` `Mathlib.Topology.UniformSpace.Equicontinuity` `Mathlib.Topology.UniformSpace.Equiv` `Mathlib.Topology.UniformSpace.HeineCantor` `Mathlib.Topology.UniformSpace.OfCompactT2` `Mathlib.Topology.UniformSpace.OfFun` `Mathlib.Topology.UniformSpace.Pi` `Mathlib.Topology.UniformSpace.Separation` `Mathlib.Topology.UniformSpace.Ultra.Basic` `Mathlib.Topology.UniformSpace.Ultra.Constructions` `Mathlib.Topology.UniformSpace.UniformConvergenceTopology` `Mathlib.Topology.UniformSpace.UniformConvergence` `Mathlib.Topology.UniformSpace.UniformEmbedding`	2
8 files `Mathlib.Computability.Ackermann` `Mathlib.Computability.Halting` `Mathlib.Computability.PartrecCode` `Mathlib.Computability.Partrec` `Mathlib.Computability.Primrec` `Mathlib.Computability.Reduce` `Mathlib.Data.Finset.Lattice.Union` `Mathlib.Logic.Godel.GodelBetaFunction`	3
`Mathlib.Algebra.Order.Ring.Finset` `Mathlib.Data.ENNReal.Lemmas`	4
`Mathlib.Algebra.Order.GroupWithZero.Finset`	5
21 files `Mathlib.Algebra.Order.Field.Pi` `Mathlib.Data.DFinsupp.Encodable` `Mathlib.Data.List.ToFinsupp` `Mathlib.Data.PFunctor.Multivariate.Basic` `Mathlib.Data.PFunctor.Multivariate.M` `Mathlib.Data.PFunctor.Multivariate.W` `Mathlib.Data.PFunctor.Univariate.Basic` `Mathlib.Data.PFunctor.Univariate.M` `Mathlib.Data.QPF.Multivariate.Basic` `Mathlib.Data.QPF.Multivariate.Constructions.Cofix` `Mathlib.Data.QPF.Multivariate.Constructions.Comp` `Mathlib.Data.QPF.Multivariate.Constructions.Const` `Mathlib.Data.QPF.Multivariate.Constructions.Fix` `Mathlib.Data.QPF.Multivariate.Constructions.Prj` `Mathlib.Data.QPF.Multivariate.Constructions.Quot` `Mathlib.Data.QPF.Multivariate.Constructions.Sigma` `Mathlib.Data.QPF.Univariate.Basic` `Mathlib.Data.W.Basic` `Mathlib.Data.W.Constructions` `Mathlib.Logic.Encodable.Pi` `Mathlib.Order.Filter.Extr`	7
9 files `Mathlib.Algebra.Order.Monoid.Canonical.Basic` `Mathlib.Data.DFinsupp.Notation` `Mathlib.Data.Finsupp.Ext` `Mathlib.Data.Finsupp.Fin` `Mathlib.Data.Finsupp.Indicator` `Mathlib.Data.Finsupp.Notation` `Mathlib.Data.Finsupp.Pointwise` `Mathlib.Data.Finsupp.SMulWithZero` `Mathlib.Data.Finsupp.Single`	8
`Mathlib.Logic.Equiv.Finset` `Mathlib.Order.CountableDenseLinearOrder`	13
6 files `Mathlib.Combinatorics.SetFamily.Compression.Down` `Mathlib.Data.Finset.Max` `Mathlib.Data.Finset.Sort` `Mathlib.Data.Fintype.Lattice` `Mathlib.Data.Fintype.Order` `Mathlib.Data.Fintype.Sort`	14
3 files `Mathlib.Data.Finset.Lattice.Fold` `Mathlib.Data.Finset.Pairwise` `Mathlib.Order.Irreducible`	15

Declarations diff

+ inf_disjSum
+ sup_disjSum

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).

b-mehta · 2025-03-16T20:54:19Z

Mathlib/Data/Finset/Sum.lean

 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Data.Finset.Card
+import Mathlib.Data.Finset.Lattice.Fold


What happens if we do the imports the other way round, that is, put these lemmas in Lattice/Fold and have that file import Sum? I'd prefer this option, since lattice operations are less fundamental than finsets on sum types

@b-mehta Now it fails by line 13 of Mathlib/Data/Finset/Max.lean, saying that Monoid is not allowed to be imported. Reverting the change.

@b-mehta, @YaelDillies: do you have any preference about leaving the lemma here vs moving it to the other file and dropping the assert_not_exists?

I think it should move to the other file, and @YaelDillies had some ideas on how definitions should be shuffled to make the assert still satisfied.

In the meantime I've created #23078 to pick up the helper lemmas which are in the right place.

I've moved the lemma and weakened the assertions; since multiset is basically the free AddCommMonoid, it seems very reasonable to me to have AddMonoid available

Of course Multiset is the free monoid; the issue is that Finset isn't!

I don't see an import change in #23020, did you link the right PR?

There used to be an import change, but @eric-wieser stole the titular change of my PR to #23079 overnight!

Mathlib/Data/Finset/Sum.lean

Split from #22983, since these don't need any new imports.

This is about 10% faster than master, but also avoids stackoverflows: ```lean #eval ((Finset.Icc 0 100000).map (.inl (β := ℕ))).toLeft.card ``` would previously fail. `aesop` is somehow capturing an unused local variable here, but `clear` sets it straight. As a bonus, this reduces the imports needed for this file.

…-disjsum-sup

YaelDillies · 2025-03-19T09:02:40Z

cc @Vierkantor since this PR now undoes their recent work

Vierkantor

I can live with Monoid being imported in Finset.Lattice.Fold/Finset.Max (the fold requires a commutative monoid structure after all, such as (max, bot)) but I really disagree with the regression in Set.Countable and downstream from that.

I would rank the disjoint sum, cardinality and finset-indexed supremum as incomparable as far as how elementary they are. Either way, it seems we'll have to decide on an ordering now. Looks like importing Finset.Lattice.Fold into Finset.Sum (as qawbecrdtey initially did) gives a bigger bump affecting fewer files, and the other way around (as the PR currently stands) a smaller bump affecting more files. My vote goes for the first option, since it seems like it is easier to resolve locally. (There is also the fact that a lot of the transitive imports of Finset.Lattice.Fold come via Data.Set.Lattice, which I am planning to split today anyway. But that's not guaranteed to improve this PR so should not be considered with too much weight.)

If we do go with the current situation, importing Finset.Sum into Finset.Lattice.Fold, I would like some comments on the assert_not_exists that got changed, to make sure we don't entirely lose track of the regression.

qawbecrdtey · 2025-03-19T09:49:23Z

Or we can simply split the file dedicated for disjSum for each container. I'm not sure if I'm following the conversation correctly, but that's my bet.

eric-wieser · 2025-03-19T10:04:11Z

I think splitting Equiv.List should fix the Set.Countable issue?

Vierkantor · 2025-03-19T10:16:44Z

The problem is, docs#Set.countable_setOf_finite_subset needs an instance of Countable (Finset α), which goes via Denumerable (Finset α), which uses Finset.sort as an injective map into List α, and so imports Finset.Sort -> Finset.Max -> Finset.Lattice.Fold.

Vierkantor · 2025-03-19T10:17:40Z

(We could instead downstream that lemma and Set.Countable.setOf_finite but I don't know if there is a good place for them.)

eric-wieser · 2025-03-19T10:22:03Z

I have a fix for that in #23092 :)

…disjsum-sup

…eanprover-community/mathlib4 into qawbecrdtey/finset-disjsum-sup

Vierkantor

I still prefer the other import direction but now I can live with either option. So no more reason to block this from my side! :)

Mathlib/Data/Finset/Lattice/Fold.lean

eric-wieser · 2025-03-19T20:26:23Z

@b-mehta, following from #22983 (comment), are you happy with the imports now that they are the other way around?

b-mehta · 2025-03-19T20:28:09Z

Yes: this is the way round I prefer. I don't want @Vierkantor's work to be undone but it seems like that's no longer happening?

eric-wieser · 2025-03-19T21:41:58Z

If we do go with the current situation, importing Finset.Sum into Finset.Lattice.Fold, I would like some comments on the assert_not_exists that got changed, to make sure we don't entirely lose track of the regression.

@Vierkantor, does this still apply, or did it only do so to the reverted changes to Set.Countable?

Vierkantor · 2025-03-19T21:44:47Z

I am okay with the regression in Finset, no need to add a comment anymore.

eric-wieser · 2025-03-20T09:16:26Z

maintainer merge

Since I was quite involved with tweaking this PR, I'd like someone else to do the final approval.

github-actions · 2025-03-20T09:16:43Z

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

Split from #22983, since these don't need any new imports.

ocfnash · 2025-03-20T09:52:27Z

Thanks all, especially for being a bit flexible on the import change :)

bors merge

Add `sup_disjSum` and `inf_disjSum`. `sup_disjSum`: ``` (s.disjSum t).sup f = (s.sup fun x ↦ f (Sum.inl x)) ⊔ (t.sup fun x ↦ f (Sum.inr x)) ``` `inf_disjSum`: ``` (s.disjSum t).inf f = (s.inf fun x ↦ f (Sum.inl x)) ⊓ (t.inf fun x ↦ f (Sum.inr x)) ``` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-03-20T10:32:23Z

Pull request successfully merged into master.

Build succeeded:

Added sup_disjSum and inf_disjSum.

9600f98

qawbecrdtey changed the title ~~feat(Mathlib/Data/Finset/Sum): Added sup_disjSum and inf_disjSum.~~ feat(Mathlib/Data/Finset/Sum): Added sup_disjSum and inf_disjSum Mar 16, 2025

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 16, 2025

github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Mar 16, 2025

b-mehta reviewed Mar 16, 2025

View reviewed changes

qawbecrdtey force-pushed the qawbecrdtey/finset-disjsum-sup branch from 1d24bea to 9600f98 Compare March 17, 2025 00:42

qawbecrdtey mentioned this pull request Mar 17, 2025

[Merged by Bors] - feat: sumPiLpEquivProdLpPiLp #22973

Closed

1 task

eric-wieser reviewed Mar 17, 2025

View reviewed changes

Mathlib/Data/Finset/Sum.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 17, 2025

View reviewed changes

Mathlib/Data/Finset/Sum.lean Outdated Show resolved Hide resolved

qawbecrdtey and others added 5 commits March 17, 2025 22:29

TODO: Work on second suggestion.

e09cffe

generalize

dba6ae8

golf boilerplate

2ee66d2

tweak

358d958

add a map lemma

fefb138

eric-wieser mentioned this pull request Mar 18, 2025

[Merged by Bors] - feat: lemmas about Finset.disjSum #23078

Closed

eric-wieser added 3 commits March 19, 2025 00:26

move lemma

094728b

weaken

336ab86

why though

ef9010f

mathlib-bors bot pushed a commit that referenced this pull request Mar 19, 2025

feat: lemmas about Finset.disjSum (#23078)

56d0af4

Split from #22983, since these don't need any new imports.

eric-wieser added 3 commits March 19, 2025 01:40

Merge remote-tracking branch 'origin/staging' into qawbecrdtey/finset…

5600bde

…-disjsum-sup

Merge branch 'master' into qawbecrdtey/finset-disjsum-sup

16e6d16

YaelDillies changed the title ~~feat(Mathlib/Data/Finset/Sum): Added sup_disjSum and inf_disjSum~~ feat(Data/Finset/Sum): supremum over a disjoint union Mar 19, 2025

Vierkantor reviewed Mar 19, 2025

View reviewed changes

eric-wieser added 3 commits March 19, 2025 13:18

Merge remote-tracking branch 'origin/master' into qawbecrdtey/finset-…

2b9af0b

…disjsum-sup

Merge branch 'qawbecrdtey/finset-disjsum-sup' of https://github.com/l…

bbe4144

…eanprover-community/mathlib4 into qawbecrdtey/finset-disjsum-sup

restore

f372343

eric-wieser requested a review from Vierkantor March 19, 2025 15:21

Vierkantor approved these changes Mar 19, 2025

View reviewed changes

Mathlib/Data/Finset/Lattice/Fold.lean Outdated Show resolved Hide resolved

sort imports

aaaef24

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 20, 2025

tukamilano pushed a commit that referenced this pull request Mar 20, 2025

feat: lemmas about Finset.disjSum (#23078)

1538f74

Split from #22983, since these don't need any new imports.

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 20, 2025

mathlib-bors bot changed the title ~~feat(Data/Finset/Sum): supremum over a disjoint union~~ [Merged by Bors] - feat(Data/Finset/Sum): supremum over a disjoint union Mar 20, 2025

mathlib-bors bot closed this Mar 20, 2025

mathlib-bors bot deleted the qawbecrdtey/finset-disjsum-sup branch March 20, 2025 10:32

Conversation

qawbecrdtey commented Mar 16, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary aaaef244d0

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

qawbecrdtey Mar 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

YaelDillies commented Mar 19, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

qawbecrdtey commented Mar 19, 2025

Uh oh!

eric-wieser commented Mar 19, 2025

Uh oh!

Vierkantor commented Mar 19, 2025

Uh oh!

Vierkantor commented Mar 19, 2025

Uh oh!

eric-wieser commented Mar 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

eric-wieser commented Mar 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

b-mehta commented Mar 19, 2025

Uh oh!

eric-wieser commented Mar 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Vierkantor commented Mar 19, 2025

Uh oh!

eric-wieser commented Mar 20, 2025

Uh oh!

github-actions bot commented Mar 20, 2025

Uh oh!

ocfnash commented Mar 20, 2025

Uh oh!

mathlib-bors bot commented Mar 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

qawbecrdtey commented Mar 16, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Mar 16, 2025 •

edited

Loading

qawbecrdtey Mar 17, 2025 •

edited

Loading

eric-wieser commented Mar 19, 2025 •

edited

Loading

eric-wieser commented Mar 19, 2025 •

edited

Loading

eric-wieser commented Mar 19, 2025 •

edited

Loading