Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 03:29 11576dbb

View on Github →

feat(set_theory/zfc): ∈ is well-founded (#15213)

Estimated changes

added theorem Set.mem_asymm
added theorem Set.mem_irrefl
added theorem Set.mem_wf
added theorem pSet.mem_asymm
added theorem pSet.mem_irrefl
added theorem pSet.mem_wf