Commit 2025-11-21 11:20 7f8e7247

View on Github →

refactor(SetTheory/ZFC): deduplicate coercion to sets (#31287) Currently, we have both ZFSet.toSet and SetLike.coe to turn a ZFSet into a Set ZFSet. This is bad for simp normal form. This PR removes the first spelling in favor of the second one.

Estimated changes

added theorem ZFSet.coe_empty
added theorem ZFSet.coe_iUnion
added theorem ZFSet.coe_image
added theorem ZFSet.coe_insert
added theorem ZFSet.coe_inter
added theorem ZFSet.coe_pair
added theorem ZFSet.coe_range
added theorem ZFSet.coe_sInter
added theorem ZFSet.coe_sUnion
added theorem ZFSet.coe_sdiff
added theorem ZFSet.coe_sep
added theorem ZFSet.coe_singleton
added theorem ZFSet.coe_subset_coe
added theorem ZFSet.coe_union
modified theorem ZFSet.ext
modified theorem ZFSet.le_def
modified theorem ZFSet.lt_def
deleted theorem ZFSet.mem_diff
modified theorem ZFSet.mem_inter
modified theorem ZFSet.mem_range
added theorem ZFSet.mem_sdiff
modified theorem ZFSet.mem_singleton
modified theorem ZFSet.mem_toSet
modified theorem ZFSet.mem_union
added theorem ZFSet.nonempty_coe
deleted theorem ZFSet.nonempty_toSet_iff
added theorem ZFSet.notMem_singleton
modified theorem ZFSet.sUnion_pair
added theorem ZFSet.sep_mem
added theorem ZFSet.sep_notMem
added theorem ZFSet.sep_subset
deleted theorem ZFSet.toSet_empty
deleted theorem ZFSet.toSet_iUnion
deleted theorem ZFSet.toSet_image
modified theorem ZFSet.toSet_inj
modified theorem ZFSet.toSet_injective
deleted theorem ZFSet.toSet_insert
deleted theorem ZFSet.toSet_inter
deleted theorem ZFSet.toSet_pair
deleted theorem ZFSet.toSet_range
deleted theorem ZFSet.toSet_sInter
deleted theorem ZFSet.toSet_sUnion
deleted theorem ZFSet.toSet_sdiff
deleted theorem ZFSet.toSet_sep
deleted theorem ZFSet.toSet_singleton
deleted theorem ZFSet.toSet_subset_iff
deleted theorem ZFSet.toSet_union