Skip to content

feat: many simp lemmas about aleph/beth/omega functions and lift#37363

Open
vihdzp wants to merge 11 commits intoleanprover-community:masterfrom
vihdzp:simplift
Open

feat: many simp lemmas about aleph/beth/omega functions and lift#37363
vihdzp wants to merge 11 commits intoleanprover-community:masterfrom
vihdzp:simplift

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Mar 30, 2026

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 30, 2026

PR summary 5ccfc60402

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ aleph_natCast_eq_lift
+ aleph_natCast_le_lift
+ aleph_natCast_lt_lift
+ aleph_ofNat_eq_lift
+ aleph_ofNat_le_lift
+ aleph_ofNat_lt_lift
+ beth_natCast_eq_lift
+ beth_natCast_le_lift
+ beth_natCast_lt_lift
+ beth_ofNat_eq_lift
+ beth_ofNat_le_lift
+ beth_ofNat_lt_lift
+ lift_eq_aleph_natCast
+ lift_eq_aleph_ofNat
+ lift_eq_beth_natCast
+ lift_eq_beth_ofNat
+ lift_eq_omega_natCast
+ lift_eq_omega_ofNat
+ lift_eq_omega_one
+ lift_le_aleph_natCast
+ lift_le_aleph_ofNat
+ lift_le_beth_natCast
+ lift_le_beth_ofNat
+ lift_le_omega_natCast
+ lift_le_omega_ofNat
+ lift_le_omega_one
+ lift_lt_aleph_natCast
+ lift_lt_aleph_ofNat
+ lift_lt_beth_natCast
+ lift_lt_beth_ofNat
+ lift_lt_omega_natCast
+ lift_lt_omega_ofNat
+ lift_lt_omega_one
+ omega_natCast_eq_lift
+ omega_natCast_le_lift
+ omega_natCast_lt_lift
+ omega_ofNat_eq_lift
+ omega_ofNat_le_lift
+ omega_ofNat_lt_lift
+ omega_one_eq_lift
+ omega_one_le_lift
+ omega_one_lt_lift

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

@vihdzp vihdzp added the t-set-theory Set theory label Mar 30, 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 30, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

This PR/issue depends on:

@vihdzp vihdzp requested a review from YaelDillies March 31, 2026 10:27
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks! 🚀

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 1, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-set-theory Set theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants