Commit 2026-09-22 23:37 2f3d8f63

refactor: change pset to a structure (#43976) I was fiddling with ZFSets when I found that replacing PSets inductive definition with a structure simplified the file. Some proofs were using the wrong API lemmas. The new definition is as follows:

structure PSet : Type (u + 1) where
  «Type» : Type u
  Func : «Type» → PSet

Zulip thread : https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/PSets.20as.20structures.3F/near/625458978