Commit 2026-09-22 13:54 b7b497b7

View on Github →

feat(Data/Finset/Sups): add infs_eq_inter and powerset_inter_eq_inter (#42520) ... 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).

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean

Modified Mathlib/Data/Finset/Sups.lean

added theorem Finset.infs_eq_inter

added theorem Finset.isLowerSet_coe_powerset

added theorem Finset.isLowerSet_preimage_coe_powerset

modified theorem Finset.powerset_infs_powerset_self

modified theorem Finset.powerset_inter

added theorem Finset.powerset_inter_eq_inter

Modified Mathlib/Data/Set/Sups.lean

added theorem Set.infs_eq_inter

added theorem Set.isLowerSet_powerset