Commit 2024-04-04 21:40 97400875

feat(Data/Set/Pairwise/Basic): pairwise disjoint sets and subsingletons (#11629) Add a lemma giving a characterization of pairwise disjoint sets in terms of each value lying in at most one set:

lemma subsingleton_setOf_mem_iff_pairwise_disjoint {f : ι → Set α} :
    (∀ a, {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Disjoint on f) :=

From AperiodicMonotilesLean.