[Merged by Bors] - chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order by YaelDillies · Pull Request #20317 · leanprover-community/mathlib4

YaelDillies · 2024-12-29T09:40:52Z

I found those lemma names hard to find, especially because they didn't contain _of_dense or didn't contain lt.

Moves:

le_of_forall_le_of_dense → le_of_forall_gt_imp_ge_of_dense
le_of_forall_ge_of_dense → le_of_forall_lt_imp_le_of_dense
forall_lt_le_iff → forall_lt_imp_le_iff_le_of_dense
forall_gt_ge_iff → forall_gt_imp_ge_iff_le_of_dense
eq_of_le_of_forall_le_of_dense → eq_of_le_of_forall_lt_imp_le_of_dense
eq_of_le_of_forall_ge_of_dense → eq_of_le_of_forall_gt_imp_ge_of_dense

This is extracted from a proof about `WithBot`/`WithTop`

github-actions · 2024-12-29T09:41:39Z

messageFile.md

Mathlib/Order/Basic.lean

b-mehta

Please list the renames you are doing in the PR description.

Mathlib/Order/Basic.lean

…_dense

github-actions · 2025-01-21T22:36:03Z

messageFile.md

github-actions · 2025-01-21T22:37:09Z

PR summary a6b8724eac

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ eq_of_le_of_forall_gt_imp_ge_of_dense
+ eq_of_le_of_forall_lt_imp_le_of_dense
+ forall_gt_imp_ge_iff_le_of_dense
+ forall_lt_imp_le_iff_le_of_dense
+ le_of_forall_gt_imp_ge_of_dense
+ le_of_forall_lt_imp_le_of_dense

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

Mathlib/Order/Basic.lean

b-mehta · 2025-01-27T14:18:59Z

Thanks!

bors merge

… order (#20317) I found those lemma names hard to find, especially because they didn't contain `_of_dense` or didn't contain `lt`. Moves: * `le_of_forall_le_of_dense` → `le_of_forall_gt_imp_ge_of_dense` * `le_of_forall_ge_of_dense` → `le_of_forall_lt_imp_le_of_dense` * `forall_lt_le_iff` → `forall_lt_imp_le_iff_le_of_dense` * `forall_gt_ge_iff` → `forall_gt_imp_ge_iff_le_of_dense` * `eq_of_le_of_forall_le_of_dense` → `eq_of_le_of_forall_lt_imp_le_of_dense` * `eq_of_le_of_forall_ge_of_dense` → `eq_of_le_of_forall_gt_imp_ge_of_dense`

mathlib-bors · 2025-01-27T15:35:36Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...

* polynomial-sequences: (308 commits) Use the lemma we already added. Minor reordering. This is true even for the trivial ring. Also add the lt versions and the other inj lemma. Also add the basis ne versions. This seems also like it should be simp. Back to sorry free. And the natDegree version. feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) ...

feat: (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂

5fc301e

This is extracted from a proof about `WithBot`/`WithTop`

github-actions bot added the t-order Order theory label Dec 29, 2024

YaelDillies mentioned this pull request Dec 29, 2024

[Merged by Bors] - refactor: define ≤/< on WithBot/WithTop by induction #19668

Closed

4 tasks

YaelDillies changed the title ~~feat: (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂~~ feat: (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ in a dense order Dec 29, 2024

fix

e50d5ee

eric-wieser reviewed Dec 30, 2024

View reviewed changes

Mathlib/Order/Basic.lean Outdated Show resolved Hide resolved

deprecate instead

d33b1e2

YaelDillies changed the title ~~feat: (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ in a dense order~~ chore: rename the fact that (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ in a dense order Dec 30, 2024

b-mehta reviewed Jan 21, 2025

View reviewed changes

Mathlib/Order/Basic.lean Show resolved Hide resolved

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 21, 2025

YaelDillies added 3 commits January 21, 2025 22:33

more renames

afcc877

fix

0b4aa1c

Merge remote-tracking branch 'origin/master' into forall_ge_iff_le_of…

7295d4b

…_dense

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 21, 2025

YaelDillies added 3 commits January 21, 2025 22:44

fix

3c01bea

long line

34ebbf2

fix

cb9ec24

b-mehta requested changes Jan 22, 2025

View reviewed changes

Mathlib/Order/Basic.lean Outdated Show resolved Hide resolved

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 22, 2025

more renames

0976392

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 23, 2025

b-mehta approved these changes Jan 23, 2025

View reviewed changes

fix

a6b8724

ghost added the ready-to-merge This PR has been sent to bors. label Jan 27, 2025

mathlib-bors bot changed the title ~~chore: rename the fact that (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ in a dense order~~ [Merged by Bors] - chore: rename the fact that (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ in a dense order Jan 27, 2025

mathlib-bors bot closed this Jan 27, 2025

mathlib-bors bot deleted the forall_ge_iff_le_of_dense branch January 27, 2025 15:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order#20317

[Merged by Bors] - chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order#20317
YaelDillies wants to merge 11 commits intomasterfrom
forall_ge_iff_le_of_dense

YaelDillies commented Dec 29, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Dec 29, 2024 •

edited

Loading

Uh oh!

Uh oh!

b-mehta left a comment

Uh oh!

Uh oh!

github-actions bot commented Jan 21, 2025

Uh oh!

github-actions bot commented Jan 21, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

b-mehta commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

YaelDillies commented Dec 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Jan 21, 2025

Uh oh!

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

Uh oh!

PR summary a6b8724eac

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

b-mehta commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

YaelDillies commented Dec 29, 2024 •

edited

Loading

github-actions bot commented Dec 29, 2024 •

edited

Loading

github-actions bot commented Jan 21, 2025 •

edited

Loading