Skip to content

[Merged by Bors] - feat(Order/WellFounded): Acc and infinite descending chain#28120

Closed
alreadydone wants to merge 11 commits intoleanprover-community:masterfrom
alreadydone:acc_decreasing_seq
Closed

[Merged by Bors] - feat(Order/WellFounded): Acc and infinite descending chain#28120
alreadydone wants to merge 11 commits intoleanprover-community:masterfrom
alreadydone:acc_decreasing_seq

Conversation

@alreadydone
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone commented Aug 8, 2025 •
edited
Loading

Open in Gitpod

@alreadydone alreadydone added t-order Order theory t-set-theory Set theory labels Aug 8, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 8, 2025 •
edited
Loading

PR summary af83bb0f64

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ acc_def
+ acc_iff_isEmpty_descending_chain
+ acc_iff_isEmpty_subtype_mem_range
+ not_acc
+ not_acc_iff_exists_descending_chain
+ not_wellFounded
+ wellFounded_iff_isEmpty
+ wellFounded_iff_isEmpty_descending_chain
++-- wellFounded_iff_no_descending_seq
+-+ exists_not_acc_lt_of_not_acc

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

alreadydone
alreadydone commented Aug 8, 2025
View reviewed changes
staroperator
staroperator reviewed Aug 8, 2025
View reviewed changes
staroperator
staroperator reviewed Aug 8, 2025
View reviewed changes
staroperator
staroperator reviewed Aug 8, 2025
View reviewed changes
@alreadydone @staroperator
Apply suggestions from code review
ba0d8f4 
Co-authored-by: staroperator <143908816+staroperator@users.noreply.github.com>
@alreadydone alreadydone mentioned this pull request Aug 9, 2025
Merged
alreadydone
alreadydone commented Aug 10, 2025
View reviewed changes
@alreadydone alreadydone changed the title feat: not_acc_iff_exists_nat_fun feat(Order/WellFounded): Acc and infinite descending chain Aug 12, 2025
b-mehta
b-mehta approved these changes Aug 12, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for this, these generalisations are valuable! I have a question about the naming, and a minor docstring comment, but this is in good shape overall.

@b-mehta b-mehta added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 12, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Aug 13, 2025

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 13, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 14, 2025
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 14, 2025
@alreadydone @b-mehta
on strict orders -> in terms of relation embeddings
0eefd74 
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
@alreadydone
Copy link
Copy Markdown
Contributor Author

alreadydone commented Aug 15, 2025 •
edited
Loading

Thanks 🎉
bors r+
(Oh it's not delegated yet ...)

@leanprover-community leanprover-community deleted a comment from mathlib-bors bot Aug 15, 2025
@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Aug 15, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Aug 15, 2025
mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025
@alreadydone
feat(Order/WellFounded): Acc and infinite descending chain (#28120)
0220769
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 15, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Order/WellFounded): Acc and infinite descending chain [Merged by Bors] - feat(Order/WellFounded): Acc and infinite descending chain Aug 15, 2025
@mathlib-bors mathlib-bors bot closed this Aug 15, 2025
Julian added a commit to Aaron1011/mathlib4 that referenced this pull request Aug 16, 2025
@Julian
Merge remote-tracking branch 'origin/master' into gromov-growth
74c41e2 
* origin/master: (508 commits)
  feat(Logic/Basic): forall_and_index (leanprover-community#27737)
  feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021)
  feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000)
  chore: more elementary Motzkin polynomial proof (leanprover-community#28482)
  feat: e-seminormed monoid (leanprover-community#27385)
  feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171)
  fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513)
  chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504)
  feat(RingTheory): invertible modules and Picard group (leanprover-community#25337)
  chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498)
  feat: add bilinear maps for vector/matrix products (leanprover-community#28130)
  feat(Counterexamples): topologists' sine curve (leanprover-community#25833)
  feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453)
  chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436)
  feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285)
  feat: make `ring` work for semifields (leanprover-community#28494)
  feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295)
  chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270)
  refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450)
  feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120)
  feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667)
  chore(*): address a few timeout-related porting notes (leanprover-community#28483)
  feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238)
  feat(Shrink): `IsCancelMul` instance (leanprover-community#28407)
  chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485)
  feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087)
  chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554)
  feat(RingTheory): faithfully flat ring maps (leanprover-community#24530)
  chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656)
  chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459)
  feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816)
  feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213)
  chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402)
  feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030)
  chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454)
  chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962)
  feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582)
  feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039)
  feat: tactic analysis framework (leanprover-community#26683)
  chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424)
  feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413)
  chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231)
  chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202)
  feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885)
  chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660)
  feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255)
  chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438)
  chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431)
  feat: separate linter error message for empty doc-strings (leanprover-community#27895)
  feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497)
  ...
@alreadydone alreadydone deleted the acc_decreasing_seq branch August 20, 2025 13:20
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@alreadydone @Paul-Lez
feat(Order/WellFounded): Acc and infinite descending chain (leanprove…
a28ccff 
…r-community#28120)
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@alreadydone @pechersky
feat(Order/WellFounded): Acc and infinite descending chain (leanprove…
c45af35 
…r-community#28120)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta approved these changes

+2 more reviewers

@vihdzp vihdzp vihdzp approved these changes

@staroperator staroperator staroperator approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-order Order theory t-set-theory Set theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@alreadydone @mathlib4-merge-conflict-bot @b-mehta @vihdzp @staroperator