Skip to content

feat: monotone function Cardinal → α is eventually constant#37344

Open
vihdzp wants to merge 3 commits intoleanprover-community:masterfrom
vihdzp:monorange
Open

feat: monotone function Cardinal → α is eventually constant#37344
vihdzp wants to merge 3 commits intoleanprover-community:masterfrom
vihdzp:monorange

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Mar 29, 2026

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 29, 2026 •
edited
Loading

PR summary e960b84129

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.SetTheory.Cardinal.EventuallyConst (new file) 728

Declarations diff

+ small_orderDual
++ eventuallyConst_of_antitone
++ eventuallyConst_of_monotone

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

wwylele
wwylele reviewed Mar 29, 2026
View reviewed changes
Mathlib/SetTheory/Cardinal/EventuallyConst.lean
have := hf <| ha (mem_range_self ⟨f b, b, rfl⟩)
rwa [apply_rangeSplitting f] at this

theorem eventuallyConst_of_antitone (hf : Antitone f) : atTop.EventuallyConst f :=
Copy link
Copy Markdown
Collaborator

@wwylele wwylele Mar 29, 2026

Choose a reason for hiding this comment

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

Can this be generated or tagged by @[to_dual]?

Copy link
Copy Markdown
Collaborator Author

@vihdzp vihdzp Mar 29, 2026

Choose a reason for hiding this comment

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

Maybe it can, but I couldn't figure out how. to_dual doesn't seem to like working with specific types such as Cardinal.

@vihdzp vihdzp added t-order Order theory t-set-theory Set theory labels Mar 29, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@wwylele wwylele wwylele left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

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.

2 participants

@vihdzp @wwylele