Theorem Finset.isEmpty_of_forall_eq_empty

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.isEmpty_of_forall_eq_emptyView on Github →