Commit 2024-08-20 21:47 fe132539
View on Github →feat(SetTheory/ZFC): Add mem_
theorems for PSet
(#16006)
There are mem_insert_iff
, mem_singleton
, mem_pair
and mem_sep
theorems for ZFSet
but no PSet
version. This PR adds them and uses them to simplify proofs in ZFSet
.