Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-21 16:19 f05fdcac

View on Github →

refactor(set_theory/zfc): make Class morally Set → Prop (#15248) We use Class in place of Set → Prop (within the Class API), and document this decision. Note that there's no longer much reason to have Class.to_Set separately from Class.mem. I will suggest inlining both into the has_mem instance in a followup PR. See Zulip).

Estimated changes

modified def Class.iota
modified theorem Class.iota_ex
modified theorem Class.iota_val
modified theorem Class.sep_hom
modified def Class.to_Set
modified theorem Class.to_Set_of_Set