Commit 2026-09-30 18:47 5d7a4fb8

View on Github →

refactor(SetTheory/ZFC): make Class an abbrev for Set ZFSet (#43467) Also take the opportunity to perform a few more changes:

  • Rename Class to ZFClass
  • Rename the coercion from ZFSet to ZFClass to ofSet in lemma names, following the naming convention. Some simp/norm_cast lemmas are becoming duplicates of lemmas about Set ZFSet in ZFC.Basic. We might want to drop the abbrev or move it earlier so as to deduplicate these lemmas, but this is out of scope for this PR. Generated by Claude Sonnet/reviewed by myself in several prompts, then subsequently heavily rewritten by hand. Assisted-by: Claude Sonnet 5

Estimated changes

added theorem Class.coe.inj
added def Class.coe
modified theorem Class.fval_ex
deleted theorem Class.ofSet.inj
deleted def Class.ofSet
added theorem ZFClass.cmem_asymm
added theorem ZFClass.cmem_irrefl
added theorem ZFClass.cmem_sInter
added theorem ZFClass.cmem_sUnion
added theorem ZFClass.cmem_univ
added theorem ZFClass.coe_cmem
added theorem ZFClass.coe_empty
added theorem ZFClass.coe_insert
added theorem ZFClass.coe_inter
added theorem ZFClass.coe_powerset
added theorem ZFClass.coe_sInter
added theorem ZFClass.coe_sUnion
added theorem ZFClass.coe_sdiff
added theorem ZFClass.coe_sep
added theorem ZFClass.coe_subset
added theorem ZFClass.coe_union
added def ZFClass.fval
added theorem ZFClass.fval_ex
added def ZFClass.iota
added theorem ZFClass.iota_ex
added theorem ZFClass.iota_val
added theorem ZFClass.mem_powerset
added theorem ZFClass.mem_sInter
added theorem ZFClass.mem_sUnion
added theorem ZFClass.notCMem_empty
added def ZFClass.powerset
added def ZFClass.sInter
added theorem ZFClass.sInter_empty
added def ZFClass.sUnion
added theorem ZFClass.sUnion_empty
added theorem ZFSet.choice_cmem
deleted theorem ZFSet.choice_mem
modified theorem ZFSet.map_fval
modified theorem ZFSet.iUnion_vonNeumann