Commit 2023-04-06 22:39 a4929f57

View on Github →

feat: port SetTheory.ZFC.Basic (#3165) A re-do of #1215, necessary since a lot of major changes have happened in the last months.

Estimated changes

added def Arity.Const
added theorem Arity.const_succ
added theorem Arity.const_succ_apply
added theorem Arity.const_zero
added def Arity
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_sep
added theorem Class.coe_subset
added theorem Class.coe_union
added theorem Class.coe_unionₛ
added theorem Class.ext
added theorem Class.ext_iff
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_unionₛ
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 theorem Class.toSet_of_setCat
added def Class.unionₛ
added theorem Class.unionₛ_apply
added theorem Class.unionₛ_empty
added def Class.univ
added def Class
added def PSet.Arity.Equiv
added theorem PSet.Arity.equiv_const
added theorem PSet.Definable.eq
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 def PSet.Resp.Equiv
added def PSet.Resp.eval
added theorem PSet.Resp.eval_val
added def PSet.Resp.f
added def PSet.Resp
added theorem PSet.Subset.congr_left
added def PSet.embed
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_irrefl
added theorem PSet.mem_powerset
added theorem PSet.mem_toSet
added theorem PSet.mem_unionₛ
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 def PSet.ofNat
added def PSet.omega
added def PSet.powerset
added def PSet.toSet
added theorem PSet.toSet_empty
added theorem PSet.toSet_unionₛ
added def PSet.unionₛ
added def PSet.«Type»
added inductive PSet
added theorem ZFSet.Hereditarily.mem
added def ZFSet.IsFunc
added theorem ZFSet.choice_isFunc
added theorem ZFSet.choice_mem
added theorem ZFSet.choice_mem_aux
added theorem ZFSet.empty_subset
added theorem ZFSet.eq
added theorem ZFSet.eq_empty
added theorem ZFSet.eval_mk
added theorem ZFSet.exact
added theorem ZFSet.ext
added theorem ZFSet.ext_iff
added def ZFSet.funs
added theorem ZFSet.hereditarily_iff
added theorem ZFSet.image.mk
added def ZFSet.image
added theorem ZFSet.inductionOn
added theorem ZFSet.insert_nonempty
added theorem ZFSet.map_fval
added theorem ZFSet.map_isFunc
added theorem ZFSet.map_unique
added theorem ZFSet.mem_asymm
added theorem ZFSet.mem_diff
added theorem ZFSet.mem_funs
added theorem ZFSet.mem_image
added theorem ZFSet.mem_insert
added theorem ZFSet.mem_insert_iff
added theorem ZFSet.mem_inter
added theorem ZFSet.mem_irrefl
added theorem ZFSet.mem_map
added theorem ZFSet.mem_pair
added theorem ZFSet.mem_pairSep
added theorem ZFSet.mem_powerset
added theorem ZFSet.mem_prod
added theorem ZFSet.mem_range
added theorem ZFSet.mem_sep
added theorem ZFSet.mem_singleton
added theorem ZFSet.mem_toSet
added theorem ZFSet.mem_union
added theorem ZFSet.mem_unionₛ
added theorem ZFSet.mem_wf
added def ZFSet.mk
added theorem ZFSet.mk_eq
added theorem ZFSet.mk_mem_iff
added theorem ZFSet.mk_out
added theorem ZFSet.nonempty_def
added theorem ZFSet.nonempty_mk_iff
added theorem ZFSet.nonempty_of_mem
added theorem ZFSet.not_mem_empty
added def ZFSet.omega
added theorem ZFSet.omega_succ
added theorem ZFSet.omega_zero
added def ZFSet.pair
added def ZFSet.pairSep
added theorem ZFSet.pair_inj
added theorem ZFSet.pair_injective
added theorem ZFSet.pair_mem_prod
added def ZFSet.powerset
added def ZFSet.prod
added theorem ZFSet.regularity
added theorem ZFSet.singleton_inj
added theorem ZFSet.sound
added theorem ZFSet.subset_def
added theorem ZFSet.subset_iff
added def ZFSet.toSet
added theorem ZFSet.toSet_empty
added theorem ZFSet.toSet_image
added theorem ZFSet.toSet_inj
added theorem ZFSet.toSet_injective
added theorem ZFSet.toSet_insert
added theorem ZFSet.toSet_inter
added theorem ZFSet.toSet_pair
added theorem ZFSet.toSet_range
added theorem ZFSet.toSet_sdiff
added theorem ZFSet.toSet_sep
added theorem ZFSet.toSet_singleton
added theorem ZFSet.toSet_subset_iff
added theorem ZFSet.toSet_union
added theorem ZFSet.to_set_unionₛ
added def ZFSet.unionₛ
added theorem ZFSet.unionₛ_empty
added theorem ZFSet.unionₛ_lem
added theorem ZFSet.unionₛ_pair
added def ZFSet
added theorem arity_succ
added theorem arity_zero