Theorem Set.univ_set_eq_singleton_empty_iff

Modification history

2025-10-19 14:27
Mathlib/Data/Set/Subsingleton.lean
chore: miscellaneous linter whitespace fixes (#30663) …
Modified Set.univ_set_eq_singleton_empty_iffView on Github →
2025-09-05 03:04
Mathlib/Data/Set/Subsingleton.lean
feat(Data/{Set, Finset}): a few easy lemmas about `Set.univ (Finset a)` and `Set.univ (Set a)` (#29238) …
Added Set.univ_set_eq_singleton_empty_iffView on Github →