Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-09 17:00 b88fa08f

View on Github →

feat(set_theory/zfc): lemmas on to_set (#15265) We also flip the direction of Set.ext_iff to match set.ext_iff.

Estimated changes

modified theorem Set.ext
modified theorem Set.ext_iff
added theorem Set.mem_to_set
added theorem Set.mk_mem_iff
added theorem Set.to_set_empty
added theorem Set.to_set_image
added theorem Set.to_set_inj
added theorem Set.to_set_injective
added theorem Set.to_set_insert
added theorem Set.to_set_inter
added theorem Set.to_set_pair
added theorem Set.to_set_sUnion
added theorem Set.to_set_sdiff
added theorem Set.to_set_sep
added theorem Set.to_set_singleton
added theorem Set.to_set_subset_iff
added theorem Set.to_set_union
added theorem pSet.mem_to_set
added theorem pSet.to_set_empty
added theorem pSet.to_set_sUnion