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 src/set_theory/zfc/basic.lean

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