Theorem List.setOf_mem_eq_empty_iff

Modification history

2026-07-17 09:57

Mathlib/Data/List/Lemmas.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Deleted List.setOf_mem_eq_empty_iff View on Github →

2025-03-21 20:58

Mathlib/Data/List/Lemmas.lean

feat(List): a list contains a single element iff it's a singleton (#20488) …

Added List.setOf_mem_eq_empty_iff View on Github →