Commit 2023-01-25 14:10 996b0ff9

View on Github →

feat(set_theory/zfc/basic): more basic simp/ext lemmas (#18233) We prove class extensionality, the characterization of class unions, and other very simple results.

Estimated changes

Modified src/set_theory/zfc/basic.lean

added theorem Class.coe_mem_powerset

added theorem Class.ext

added theorem Class.ext_iff

added theorem Class.mem_sUnion

added theorem Class.not_mem_empty

added theorem Class.sUnion_empty

added theorem Set.sUnion_empty