Theorem Set.eq_mem_setOf

Modification history

2026-07-17 09:57
Mathlib/Data/Set/Operations.lean
chore(Data): rename `setOf` to `Set.ofPred` (#41507) …
Deleted Set.eq_mem_setOfView on Github →
2025-06-12 11:49
Mathlib/Data/Set/Basic.lean
chore(Data/Set): move very basic lemmas earlier (#25707) …
Modified Set.eq_mem_setOfView on Github →
2024-08-07 06:03
Mathlib/Data/Set/Basic.lean
chore(Data/Set/Basic): predicate is equal to membership in setOf. (#15554) …
Added Set.eq_mem_setOfView on Github →