Theorem Set.univ_set_of_isEmpty

Modification history

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_of_isEmpty View on Github →