Commit 2025-09-05 03:04 90c27465

View on Github →

feat(Data/{Set, Finset}): a few easy lemmas about Set.univ (Finset a) and Set.univ (Set a) (#29238) Upstreamed from formal-conjectures (see google-deepmind/formal-conjectures#551)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.isEmpty_of_forall_eq_empty

modified theorem Finset.mem_union_of_disjoint

added theorem Finset.univ_finset_eq_singleton_empty_iff

added theorem Finset.univ_finset_of_isEmpty

Modified Mathlib/Data/Set/Subsingleton.lean

added theorem Set.univ_set_eq_singleton_empty_iff

added theorem Set.univ_set_of_isEmpty