Commit 2025-10-06 15:37 95fae5db

View on Github →

feat(Data/Set/Subsingleton): added new lemma Subsingleton.union_subsingleton along with some trivial code cleanup (#29955)

Estimated changes

Modified Mathlib/Data/Set/Subsingleton.lean

modified theorem Set.subsingleton_isBot

modified theorem Set.subsingleton_isTop

modified theorem Set.subsingleton_of_subsingleton

added theorem Set.subsingleton_of_subsingleton_inter_left

added theorem Set.subsingleton_of_subsingleton_inter_right