Commit 2025-03-27 04:48 4e2055c2

View on Github →

chore: split SetTheory.ZFC.Basic (#23354) SetTheory.ZFC.Basic splits naturally into

  • .PSet for pre-sets
  • .Basic for actual ZFC sets
  • .Class for classes (the Burali-Forti paradox has also been moved here)

Estimated changes

deleted def Class.ToSet
deleted def Class.classToCong
deleted theorem Class.classToCong_empty
deleted theorem Class.coe_apply
deleted theorem Class.coe_diff
deleted theorem Class.coe_empty
deleted theorem Class.coe_insert
deleted theorem Class.coe_inter
deleted theorem Class.coe_mem
deleted theorem Class.coe_powerset
deleted theorem Class.coe_sInter
deleted theorem Class.coe_sUnion
deleted theorem Class.coe_sep
deleted theorem Class.coe_subset
deleted theorem Class.coe_union
deleted def Class.congToClass
deleted theorem Class.congToClass_empty
deleted theorem Class.eq_univ_iff_forall
deleted theorem Class.eq_univ_of_forall
deleted theorem Class.ext
deleted def Class.fval
deleted theorem Class.fval_ex
deleted def Class.iota
deleted theorem Class.iota_ex
deleted theorem Class.iota_val
deleted theorem Class.mem_asymm
deleted theorem Class.mem_def
deleted theorem Class.mem_irrefl
deleted theorem Class.mem_of_mem_sInter
deleted theorem Class.mem_sInter
deleted theorem Class.mem_sUnion
deleted theorem Class.mem_univ
deleted theorem Class.mem_univ_hom
deleted theorem Class.mem_wf
deleted theorem Class.not_empty_hom
deleted theorem Class.not_mem_empty
deleted theorem Class.ofSet.inj
deleted def Class.ofSet
deleted def Class.powerset
deleted theorem Class.powerset_apply
deleted def Class.sInter
deleted theorem Class.sInter_apply
deleted theorem Class.sInter_empty
deleted def Class.sUnion
deleted theorem Class.sUnion_apply
deleted theorem Class.sUnion_empty
deleted theorem Class.toSet_of_ZFSet
deleted def Class.univ
deleted theorem Class.univ_not_mem_univ
deleted def Class
deleted theorem PSet.Equiv.eq
deleted theorem PSet.Equiv.exists_left
deleted theorem PSet.Equiv.exists_right
deleted theorem PSet.Equiv.ext
deleted def PSet.Equiv
deleted def PSet.Func
deleted theorem PSet.Mem.congr_left
deleted theorem PSet.Mem.congr_right
deleted theorem PSet.Mem.ext
deleted theorem PSet.Mem.mk
deleted theorem PSet.Subset.congr_left
deleted theorem PSet.Subset.congr_right
deleted def PSet.embed
deleted theorem PSet.empty_def
deleted theorem PSet.empty_subset
deleted theorem PSet.equiv_iff
deleted theorem PSet.equiv_iff_mem
deleted theorem PSet.eta
deleted theorem PSet.func_mem
deleted def PSet.image
deleted theorem PSet.lift_mem_embed
deleted theorem PSet.mem_asymm
deleted theorem PSet.mem_image
deleted theorem PSet.mem_insert
deleted theorem PSet.mem_insert_iff
deleted theorem PSet.mem_insert_of_mem
deleted theorem PSet.mem_irrefl
deleted theorem PSet.mem_of_subset
deleted theorem PSet.mem_pair
deleted theorem PSet.mem_powerset
deleted theorem PSet.mem_sUnion
deleted theorem PSet.mem_sep
deleted theorem PSet.mem_singleton
deleted theorem PSet.mem_toSet
deleted theorem PSet.mem_wf
deleted theorem PSet.mk_func
deleted theorem PSet.mk_type
deleted theorem PSet.nonempty_def
deleted theorem PSet.nonempty_of_mem
deleted theorem PSet.nonempty_toSet_iff
deleted theorem PSet.not_mem_empty
deleted theorem PSet.not_mem_of_subset
deleted theorem PSet.not_nonempty_empty
deleted theorem PSet.not_subset_of_mem
deleted def PSet.ofNat
deleted def PSet.omega
deleted def PSet.powerset
deleted def PSet.sUnion
deleted theorem PSet.subset_iff
deleted def PSet.toSet
deleted theorem PSet.toSet_empty
deleted theorem PSet.toSet_sUnion
deleted def PSet.«Type»
deleted inductive PSet
deleted theorem ZFSet.choice_isFunc
deleted theorem ZFSet.choice_mem
deleted theorem ZFSet.choice_mem_aux
deleted theorem ZFSet.map_fval
added def Class.ToSet
added theorem Class.coe_apply
added theorem Class.coe_diff
added theorem Class.coe_empty
added theorem Class.coe_insert
added theorem Class.coe_inter
added theorem Class.coe_mem
added theorem Class.coe_powerset
added theorem Class.coe_sInter
added theorem Class.coe_sUnion
added theorem Class.coe_sep
added theorem Class.coe_subset
added theorem Class.coe_union
added theorem Class.ext
added def Class.fval
added theorem Class.fval_ex
added def Class.iota
added theorem Class.iota_ex
added theorem Class.iota_val
added theorem Class.mem_asymm
added theorem Class.mem_def
added theorem Class.mem_irrefl
added theorem Class.mem_sInter
added theorem Class.mem_sUnion
added theorem Class.mem_univ
added theorem Class.mem_univ_hom
added theorem Class.mem_wf
added theorem Class.not_empty_hom
added theorem Class.not_mem_empty
added theorem Class.ofSet.inj
added def Class.ofSet
added def Class.powerset
added theorem Class.powerset_apply
added def Class.sInter
added theorem Class.sInter_apply
added theorem Class.sInter_empty
added def Class.sUnion
added theorem Class.sUnion_apply
added theorem Class.sUnion_empty
added theorem Class.toSet_of_ZFSet
added def Class.univ
added def Class
added theorem ZFSet.choice_isFunc
added theorem ZFSet.choice_mem
added theorem ZFSet.choice_mem_aux
added theorem ZFSet.map_fval
added theorem PSet.Equiv.eq
added theorem PSet.Equiv.exists_left
added theorem PSet.Equiv.ext
added def PSet.Equiv
added def PSet.Func
added theorem PSet.Mem.congr_left
added theorem PSet.Mem.congr_right
added theorem PSet.Mem.ext
added theorem PSet.Mem.mk
added theorem PSet.Subset.congr_left
added def PSet.embed
added theorem PSet.empty_def
added theorem PSet.empty_subset
added theorem PSet.equiv_iff
added theorem PSet.equiv_iff_mem
added theorem PSet.eta
added theorem PSet.func_mem
added def PSet.image
added theorem PSet.lift_mem_embed
added theorem PSet.mem_asymm
added theorem PSet.mem_image
added theorem PSet.mem_insert
added theorem PSet.mem_insert_iff
added theorem PSet.mem_insert_of_mem
added theorem PSet.mem_irrefl
added theorem PSet.mem_of_subset
added theorem PSet.mem_pair
added theorem PSet.mem_powerset
added theorem PSet.mem_sUnion
added theorem PSet.mem_sep
added theorem PSet.mem_singleton
added theorem PSet.mem_toSet
added theorem PSet.mem_wf
added theorem PSet.mk_func
added theorem PSet.mk_type
added theorem PSet.nonempty_def
added theorem PSet.nonempty_of_mem
added theorem PSet.not_mem_empty
added theorem PSet.not_mem_of_subset
added theorem PSet.not_subset_of_mem
added def PSet.ofNat
added def PSet.omega
added def PSet.powerset
added def PSet.sUnion
added theorem PSet.subset_iff
added def PSet.toSet
added theorem PSet.toSet_empty
added theorem PSet.toSet_sUnion
added def PSet.«Type»
added inductive PSet