Theorem Finset.univ_finset_eq_singleton_empty_iff

Modification history

2025-09-05 03:04
Mathlib/Data/Finset/Basic.lean
feat(Data/{Set, Finset}): a few easy lemmas about `Set.univ (Finset a)` and `Set.univ (Set a)` (#29238) …
Added Finset.univ_finset_eq_singleton_empty_iffView on Github →