[Merged by Bors] - feat: `LinearOrder` instance for `Empty` by YanYablonovskiy · Pull Request #31889 · leanprover-community/mathlib4

YanYablonovskiy · 2025-11-21T12:05:38Z

Adds a LinearOrder instance on Empty, is required for defining order types, and complements the PUnit LinearOrder instance below it.

Edit: Refactors LinearOrder on PUnit , and defined an instance on Empty and PEmpty via an instance on Subsingleton.

github-actions · 2025-11-21T12:06:38Z

PR summary b3cf7a02d3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ LinearOrder.ofSubsingleton
+ instance : LinearOrder Empty := .ofSubsingleton
+ instance : LinearOrder PEmpty := .ofSubsingleton

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

github-actions · 2025-11-21T12:06:56Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

YaelDillies

Thanks!

maintainer delegate

Mathlib/Order/Basic.lean

github-actions · 2025-11-21T12:07:37Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

Mathlib/Order/Basic.lean

Added `Empty.linearOrder` with signature `(α : Type*) -> [inst : IsEmpty α] -> LinearOrder α` , in order to register instances of `LinearOrder` on `Empty` and `PEmpty`.

Mathlib/Order/Basic.lean

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

Mathlib/Order/Basic.lean

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

Mathlib/Order/Basic.lean

…bsingleton`

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2025-11-22T10:18:12Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Mathlib/Order/Basic.lean

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

Mathlib/Order/Basic.lean

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

ocfnash · 2025-11-22T13:05:34Z

bors merge

Adds a LinearOrder instance on Empty, is required for defining order types, and complements the PUnit LinearOrder instance below it. Edit: Refactors LinearOrder on PUnit , and defined an instance on Empty and PEmpty via an instance on Subsingleton. Co-authored-by: YanYablonovskiy <yablonovskiy.yan@gmail.com>

mathlib-bors · 2025-11-22T14:21:34Z

Pull request successfully merged into master.

Build succeeded:

…lib4 * 'master' of https://github.com/leanprover-community/mathlib4: (3130 commits) feat(SetTheory/ZFC): add `ZFSet.card` (leanprover-community#29365) feat: grind annotations for `choose_spec` (leanprover-community#31927) chore(scripts): update nolints.json (leanprover-community#31975) feat(Analysis): cos (n * π) = (-1) ^ n (leanprover-community#31971) chore: rename `mul_le_mul_right'` to `mul_le_mul_left` (leanprover-community#30242) chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31955) feat(MeasureTheory): ae-measurability notation wrt non-standard sigma-algebra (leanprover-community#31910) doc: add missing spaces around doc code blocks (leanprover-community#31917) chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31945) chore: shortcut instance for `Nat` to be mul-torsion-free (leanprover-community#31027) doc(Topology/Algebra/Algebra): outdated TODO (leanprover-community#31944) feat(EqHaar): add `addHaar_nnreal_smul` (leanprover-community#31922) chore(Algebra): make invertibleInv an instance (leanprover-community#31916) chore(Algebra): change two statements in CubicDiscriminant (leanprover-community#31912) chore(MeasureTheory): mark `map_dirac` as simp (leanprover-community#31909) feat: `LinearOrder` instance for `Empty` (leanprover-community#31889) chore: deprecate all remaining modules in `Analysis/NormedSpace` (leanprover-community#31913) feat(SimpleGraph): weaker condition for paths in acyclic graphs (leanprover-community#25814) chore: do not set `group` when declaring option (leanprover-community#31888) chore: clean up more unused `Decidable*` instances in types (leanprover-community#31934) ...

Update Basic.lean

77d2c42

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Nov 21, 2025

YaelDillies changed the title ~~Add a LinearOrder instance on Empty~~ feat: LinearOrder instance for Empty Nov 21, 2025

github-actions bot added the t-order Order theory label Nov 21, 2025

YaelDillies approved these changes Nov 21, 2025

View reviewed changes

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

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

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 21, 2025

Apply suggestions from code review

72613a9

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

jcommelin reviewed Nov 21, 2025

View reviewed changes

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

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Nov 21, 2025

YanYablonovskiy added 2 commits November 22, 2025 13:49

Merge branch 'leanprover-community:master' into Empty.instLinearOrder

eeca66e

Added Empty.linearOrder α for any IsEmpty α

f57ed6c

Added `Empty.linearOrder` with signature `(α : Type*) -> [inst : IsEmpty α] -> LinearOrder α` , in order to register instances of `LinearOrder` on `Empty` and `PEmpty`.

YaelDillies reviewed Nov 22, 2025

View reviewed changes

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

YaelDillies reviewed Nov 22, 2025

View reviewed changes

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

YanYablonovskiy and others added 2 commits November 22, 2025 17:31

Update Mathlib/Order/Basic.lean

d633891

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

Fix gaff

198ba27

YaelDillies reviewed Nov 22, 2025

View reviewed changes

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

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

Apply suggestions from code review

e513a3d

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

YaelDillies reviewed Nov 22, 2025

View reviewed changes

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

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

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

Mathlib/Order/Basic.lean Show resolved Hide resolved

YanYablonovskiy added 5 commits November 22, 2025 19:37

Refactor LinearOrder instances on Empty/Unit via Subsingleton

ea55860

Add docstring + fix of trivial for tactic mode

8a5462e

Reverse unneeded changes due to changed synth order + fixes

be1edc7

Add PEmpty instance

7053213

Getting rid of unneeded tactics

ce456ed

YaelDillies reviewed Nov 22, 2025

View reviewed changes

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

Reverse changes due to / and further refactoring of `LinearOrder.ofSu…

6cf7921

…bsingleton`

YaelDillies approved these changes Nov 22, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 22, 2025

YaelDillies reviewed Nov 22, 2025

View reviewed changes

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

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

YanYablonovskiy and others added 4 commits November 22, 2025 21:20

Apply suggestions from code review

0ada94a

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

Fix a few typos

e0391ca

Fix spacing

beba6ba

Remove redundant class assumption

50dc67e

YaelDillies reviewed Nov 22, 2025

View reviewed changes

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

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

Apply suggestions from code review

21b74f5

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

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

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 Nov 22, 2025

mathlib-bors bot changed the title ~~feat: LinearOrder instance for Empty~~ [Merged by Bors] - feat: LinearOrder instance for Empty Nov 22, 2025

mathlib-bors bot closed this Nov 22, 2025

YanYablonovskiy deleted the Empty.instLinearOrder branch November 26, 2025 07:43

YanYablonovskiy mentioned this pull request Jan 16, 2026

[Merged by Bors] - feat(Order): order types #34034

Closed

2 tasks

Conversation

YanYablonovskiy commented Nov 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary b3cf7a02d3

Import changes for modified files

Declarations diff

Uh oh!

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

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Nov 21, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Nov 22, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ocfnash commented Nov 22, 2025

Uh oh!

mathlib-bors bot commented Nov 22, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

YanYablonovskiy commented Nov 21, 2025 •

edited

Loading

github-actions bot commented Nov 21, 2025 •

edited

Loading

github-actions bot commented Nov 21, 2025 •

edited

Loading