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.

Estimated changes

added theorem PSet.mem_insert
added theorem PSet.mem_insert_iff
added theorem PSet.mem_insert_of_mem
added theorem PSet.mem_of_subset
added theorem PSet.mem_pair
added theorem PSet.mem_sep
added theorem PSet.mem_singleton
added theorem PSet.subset_iff