Skip to content

refactor(Data/Finset/Sups): rename powerset_union/inter - #42520

Open
mo271 wants to merge 2 commits into
leanprover-community:masterfrom
mo271:powerset_sups_rename
Open

refactor(Data/Finset/Sups): rename powerset_union/inter#42520
mo271 wants to merge 2 commits into
leanprover-community:masterfrom
mo271:powerset_sups_rename

Conversation

@mo271

@mo271 mo271 commented Aug 7, 2026

Copy link
Copy Markdown
Collaborator

... to powerset_sups/infs

Rename Finset.powerset_union to Finset.powerset_sups and Finset.powerset_inter to Finset.powerset_infs to reflect that they compute pointwise operations and .

Add deprecation aliases.

A follow-up (#42521) will add Finset.powerset_inter back (with a different meaning).


Open in Gitpod

…ups/infs

Rename `Finset.powerset_union` to `Finset.powerset_sups` and `Finset.powerset_inter` to `Finset.powerset_infs` to reflect that they compute pointwise operations `⊻` and `⊼`.

Add deprecation alias for `Finset.powerset_union`.
@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown

PR summary 791d258ca7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

+ powerset_infs
+ powerset_sups

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

Lean-aware diff — post-build, computed from the Lean environment (commit 791d258).

  • +2 new declarations
  • −0 removed declarations
+Finset.powerset_infs
+Finset.powerset_sups

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 791d258ca7
Reference commit e506e4611d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown

✅ PR Title Formatted Correctly

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

@github-actions github-actions Bot added the t-data Data (lists, quotients, numbers, etc) label Aug 7, 2026
@mo271 mo271 changed the title refactor(Data/Finset/Sups): rename powerset_union/inter ... refactor(Data/Finset/Sups): rename powerset_union/inter Aug 7, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant