Theorem Set.subsingleton_of_subsingleton_inter_right

Modification history

2025-10-06 15:37
Mathlib/Data/Set/Subsingleton.lean
feat(Data/Set/Subsingleton): added new lemma `Subsingleton.union_subsingleton` along with some trivial code cleanup (#29955)
Added Set.subsingleton_of_subsingleton_inter_rightView on Github →