Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-30 00:32 229f6f14

View on Github →

feat(set_theory/zfc/basic): define Set and Class intersection (#18232)

Estimated changes

Modified src/set_theory/zfc/basic.lean

added theorem Class.mem_of_mem_sInter

added theorem Class.mem_sInter

added def Class.sInter

added theorem Class.sInter_apply

added theorem Class.sInter_coe

added theorem Class.sInter_empty

modified theorem Class.sUnion_empty

added theorem Set.mem_of_mem_sInter

added theorem Set.mem_sInter

added theorem Set.not_mem_sInter_of_not_mem

added theorem Set.sInter_empty

added theorem Set.sInter_singleton

modified theorem Set.sUnion_empty

added theorem Set.to_set_sInter