Zulip Chat Archive
Stream: Is there code for X?
Topic: Union of singletons
Yaël Dillies (Jan 14 2022 at 17:19):
Do we have this anywhere?
import data.set.lattice
lemma bUnion_singleton_eq {α : Type*} {s : set α} : (⋃ x ∈ s, {x}) = s := by { ext, simp }
Mario Carneiro (Jan 14 2022 at 17:20):
Yaël Dillies (Jan 14 2022 at 17:20):
Yes, we do :)
Yaël Dillies (Jan 14 2022 at 17:20):
Always trust squeeze_simp
Last updated: May 02 2025 at 03:31 UTC