Commit 2026-02-17 21:47 14e8b452

View on Github →

feat(Data/Set/PowersetCard): definitions on Set.powersetCard (#35432) This PR adds three new definitions for Set.powersetCard:

  • ofCard: casts a set of cardinality n to its corresponding element of Set.powersetCard α n
  • disjUnion: the disjoint union of finite sets as a function on Set.powersetCard
  • prodEquiv: the equivalence (n : ℕ) × (Set.powersetCard α n) ≃ Finset α

Estimated changes