Theorem Set.singleton_inter_of_mem

Modification history

2026-10-31 04:12

Mathlib/Data/Set/Insert.lean

feat: use `max`/`min` for `union`/`inter` in `Set`, `Finset`, `ZFSet`, `Class` (#42316) …

Modified Set.singleton_inter_of_mem View on Github →

2025-11-24 07:57

Mathlib/Data/Set/Insert.lean

feat: make sure that simp computes `{a} ∩ s` (#31947) …

Added Set.singleton_inter_of_mem View on Github →