Theorem Set.inter_singleton_of_mem

Modification history

2025-11-24 07:57
Mathlib/Data/Set/Insert.lean
feat: make sure that simp computes `{a} ∩ s` (#31947) …
Added Set.inter_singleton_of_memView on Github →