Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-26 09:45 7a1cc03e

View on Github →

chore(set_theory/zfc/basic): mem_empty → not_mem_empty (#18262) Matches set.not_mem_empty.

Estimated changes

deleted theorem Set.mem_empty
added theorem Set.not_mem_empty
deleted theorem pSet.mem_empty
added theorem pSet.not_mem_empty
modified theorem Set.empty_is_transitive