Skip to content

feat(Order/OmegaCompletePartialOrder): add OmegaCompletePartialOrder instance for Option with basic ωScottContinuous lemmas#34093

Closed
YellPika wants to merge 5 commits intoleanprover-community:masterfrom
YellPika:omega-complete-partial-order-option
Closed

feat(Order/OmegaCompletePartialOrder): add OmegaCompletePartialOrder instance for Option with basic ωScottContinuous lemmas#34093
YellPika wants to merge 5 commits intoleanprover-community:masterfrom
YellPika:omega-complete-partial-order-option

Conversation

@YellPika
Copy link
Copy Markdown
Contributor

@YellPika YellPika commented Jan 18, 2026 •
edited by Komyyy
Loading

@github-actions github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! large-import Automatically added label for PRs with a significant increase in transitive imports labels Jan 18, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 18, 2026 •
edited
Loading

PR summary 03cf4f1c3d

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Order.OmegaCompletePartialOrder 397 399 +2 (+0.50%)
Import changes for all files
Files Import difference
There are 3856 files with changed transitive imports taking up over 177434 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

Declarations diff

+ Monotone.ite
+ Monotone.ite'
+ bind_mono
+ coe_const
+ coe_dropOption
+ coe_some
+ const
+ dropOption
+ dropOption_some
+ get_mono
+ instance : Bot (Option α)
+ instance : OmegaCompletePartialOrder (Option α)
+ instance [LE α] : OrderBot (Option α)
+ instance [PartialOrder α] : PartialOrder (Option α)
+ instance [Preorder α] : Preorder (Option α)
+ isSome_mono
+ map_mono
+ none_eq_ωSup_iff
+ option_cases
+ some
+ some_mono
+ toOption
+ toOption_none
+ toOption_some
+ ωScottContinuous.map_ωSup₂
+ ωScottContinuous_bind
+ ωScottContinuous_map
+ ωScottContinuous_some
+ ωSup_const
+ ωSup_eq_none_iff
+ ωSup_some

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/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 mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 18, 2026
@joneugster joneugster added the t-order Order theory label Jan 18, 2026
@YellPika
Copy link
Copy Markdown
Contributor Author

YellPika commented Jan 20, 2026

WIP

@github-actions github-actions bot added the WIP Work in progress label Jan 20, 2026
@YellPika YellPika force-pushed the omega-complete-partial-order-option branch 2 times, most recently from 8f5ae92 to 3d30efb Compare January 20, 2026 22:47
@YellPika
Copy link
Copy Markdown
Contributor Author

YellPika commented Jan 20, 2026

-WIP

@github-actions github-actions bot removed the WIP Work in progress label Jan 20, 2026
@YellPika YellPika changed the title feat(Order/OmegaCompletePartialOrder): add OmegaCompletePartialOrder instance for Option feat(Order/OmegaCompletePartialOrder): add OmegaCompletePartialOrder instance for Option with basic ωScottContinuous lemmas Jan 20, 2026
@YellPika YellPika force-pushed the omega-complete-partial-order-option branch from 3d30efb to ff4f15f Compare January 21, 2026 20:14
@mathlib-merge-conflicts mathlib-merge-conflicts 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 Feb 3, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 3, 2026

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

@YellPika YellPika force-pushed the omega-complete-partial-order-option branch from ff4f15f to 24bd1ae Compare February 4, 2026 04:02
@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Feb 4, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 4, 2026
@mathlib-triage mathlib-triage bot assigned Komyyy and unassigned pechersky Mar 22, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Mar 31, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Apr 2, 2026

This PR/issue depends on:

@Komyyy
Copy link
Copy Markdown
Contributor

Komyyy commented Apr 5, 2026

@YellPika

Sorry for the late review! I've been busy lately.

I review now.

Komyyy
Komyyy requested changes Apr 5, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Thank you for your contribution! I read your Zulip thread and repository.

Could you use WithBot instead of Option? WithBot has the same order structure as Option, but has a much richer API. The order structure for Option was added as internal prototype code in the vary early days of Lean 4 (see this commit), so the API is poor. By contrast, the theory of WithBot has been well-developed since Lean 3.

@Komyyy Komyyy added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 5, 2026
@YellPika
feat(Order/OmegaCompletePartialOrder): add OmegaCompletePartialOrder …
d9cf840 
…instance for Option with basic ωScottContinuous lemmas
@YellPika YellPika force-pushed the omega-complete-partial-order-option branch from a96f9db to ae007c8 Compare April 6, 2026 15:38
@YellPika
Copy link
Copy Markdown
Contributor Author

YellPika commented Apr 6, 2026

@Komyyy Thank you for looking at this. I can certainly use WithBot. Is the plan to upstream WithBot and deprecate Option? I am wondering if I should be replacing Option with WithBot in this PR or supporting both of them.

@YellPika
Copy link
Copy Markdown
Contributor Author

YellPika commented Apr 6, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 6, 2026
@Komyyy
Copy link
Copy Markdown
Contributor

Komyyy commented Apr 7, 2026

The order structure of Option has a problem: it differs from the structure that comes up naturally from its name (which is the same as that of Part). Hence it may be changed in the future.

On the other hand, the order structure of WithBot is clear by its name, so it will not be changed.

If you want to use operations of Option in terms of a quasi-Borel space, you can use Part instead. Option should be deprecated.

@YellPika
Copy link
Copy Markdown
Contributor Author

YellPika commented Apr 9, 2026

Sorry for the delay. The changes you've requested are significant, so I have put them in a new pull request.

See #37819.

@YellPika YellPika closed this Apr 9, 2026
@YellPika YellPika mentioned this pull request Apr 9, 2026
Open
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Komyyy Komyyy Komyyy requested changes

Assignees

@Komyyy Komyyy

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@YellPika @Komyyy @pechersky @joneugster @mathlib4-dependent-issues-bot