Mathlib.Data.Finset.Pairwise

instDecidablePairwiseToSetOfDecidableEqOfDecidableRel instance

[DecidableEq α] {r : α → α → Prop} [DecidableRel r] {s : Finset α} : Decidable ((s : Set α).Pairwise r)

Full source

instance [DecidableEq α] {r : α → α → Prop} [DecidableRel r] {s : Finset α} :
    Decidable ((s : Set α).Pairwise r) :=
  decidable_of_iff' (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) Iff.rfl

Decidability of Pairwise Relations on Finite Sets

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality and a decidable relation $r$ on $\alpha$, the property that $r$ holds pairwise on $s$ (i.e., for any two distinct elements $x, y \in s$, $r(x, y)$ holds) is decidable.

Finset.pairwiseDisjoint_range_singleton theorem

: (Set.range (singleton : α → Finset α)).PairwiseDisjoint id

Full source

theorem Finset.pairwiseDisjoint_range_singleton :
    (Set.range (singleton : α → Finset α)).PairwiseDisjoint id := by
  rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
  exact disjoint_singleton.2 (ne_of_apply_ne _ h)

Pairwise Disjointness of Singleton Sets in Range

Informal description

The range of the singleton map $\{\cdot\} : \alpha \to \text{Finset } \alpha$ is pairwise disjoint under the identity function. That is, for any two distinct elements $a, b \in \alpha$, the singleton sets $\{a\}$ and $\{b\}$ are disjoint.

Set.PairwiseDisjoint.elim_finset theorem

 {s : Set ι} {f : ι → Finset α} (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (a : α) (hai : a ∈ f i)
  (haj : a ∈ f j) : i = j

Full source

theorem PairwiseDisjoint.elim_finset {s : Set ι} {f : ι → Finset α} (hs : s.PairwiseDisjoint f)
    {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (a : α) (hai : a ∈ f i) (haj : a ∈ f j) : i = j :=
  hs.elim hi hj (Finset.not_disjoint_iff.2 ⟨a, hai, haj⟩)

Equality of Indices for Common Elements in Pairwise Disjoint Finite Sets

Informal description

Let $s$ be a set of indices, and let $f \colon \iota \to \text{Finset } \alpha$ be a function mapping each index to a finite subset of $\alpha$. If $s$ is pairwise disjoint under $f$, then for any two indices $i, j \in s$ and any element $a \in \alpha$ such that $a$ belongs to both $f(i)$ and $f(j)$, we have $i = j$.

Set.PairwiseDisjoint.image_finset_of_le theorem

 [DecidableEq ι] {s : Finset ι} {f : ι → α} (hs : (s : Set ι).PairwiseDisjoint f) {g : ι → ι}
  (hf : ∀ a, f (g a) ≤ f a) : (s.image g : Set ι).PairwiseDisjoint f

Full source

theorem PairwiseDisjoint.image_finset_of_le [DecidableEq ι] {s : Finset ι} {f : ι → α}
    (hs : (s : Set ι).PairwiseDisjoint f) {g : ι → ι} (hf : ∀ a, f (g a) ≤ f a) :
    (s.image g : Set ι).PairwiseDisjoint f := by
  rw [coe_image]
  exact hs.image_of_le hf

Image of Pairwise Disjoint Finite Set under Monotone Function Preserves Pairwise Disjointness

Informal description

Let $\iota$ be a type with decidable equality, $s$ a finite subset of $\iota$, and $f \colon \iota \to \alpha$ a function where $\alpha$ is a meet-semilattice with a bottom element. If $s$ is pairwise disjoint under $f$ (i.e., for any distinct $i, j \in s$, $f(i) \sqcap f(j) = \bot$), and $g \colon \iota \to \iota$ is a function such that $f(g(a)) \leq f(a)$ for all $a \in \iota$, then the image of $s$ under $g$ (as a set) is also pairwise disjoint under $f$.

Set.PairwiseDisjoint.attach theorem

(hs : (s : Set ι).PairwiseDisjoint f) : (s.attach : Set { x // x ∈ s }).PairwiseDisjoint (f ∘ Subtype.val)

Full source

theorem PairwiseDisjoint.attach (hs : (s : Set ι).PairwiseDisjoint f) :
    (s.attach : Set { x // x ∈ s }).PairwiseDisjoint (f ∘ Subtype.val) := fun i _ j _ hij =>
  hs i.2 j.2 <| mt Subtype.ext_val hij

Pairwise Disjointness Preserved Under Attachment

Informal description

Let $s$ be a set of elements of type $\iota$, and let $f \colon \iota \to \alpha$ be a function. If $s$ is pairwise disjoint under $f$, then the attached set $\{x \mid x \in s\}$ (where each element is paired with a proof of its membership in $s$) is also pairwise disjoint under the composition $f \circ \text{Subtype.val}$, where $\text{Subtype.val}$ is the projection from the subtype to the original type $\iota$.

Set.PairwiseDisjoint.biUnion_finset theorem

 {s : Set ι'} {g : ι' → Finset ι} {f : ι → α} (hs : s.PairwiseDisjoint fun i' : ι' => (g i').sup f)
  (hg : ∀ i ∈ s, (g i : Set ι).PairwiseDisjoint f) : (⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f

Full source

/-- Bind operation for `Set.PairwiseDisjoint`. In a complete lattice, you can use
`Set.PairwiseDisjoint.biUnion`. -/
theorem PairwiseDisjoint.biUnion_finset {s : Set ι'} {g : ι' → Finset ι} {f : ι → α}
    (hs : s.PairwiseDisjoint fun i' : ι' => (g i').sup f)
    (hg : ∀ i ∈ s, (g i : Set ι).PairwiseDisjoint f) : (⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f := by
  rintro a ha b hb hab
  simp_rw [Set.mem_iUnion] at ha hb
  obtain ⟨c, hc, ha⟩ := ha
  obtain ⟨d, hd, hb⟩ := hb
  obtain hcd | hcd := eq_or_ne (g c) (g d)
  · exact hg d hd (by rwa [hcd] at ha) hb hab
  · exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)

Pairwise Disjointness of Union of Finite Sets under Suprema Condition

Informal description

Let $s$ be a set of indices of type $\iota'$, and for each $i' \in s$, let $g(i')$ be a finite set of indices of type $\iota$. Let $f \colon \iota \to \alpha$ be a function where $\alpha$ is a lattice with a bottom element $\bot$. Suppose that: 1. The set $s$ is pairwise disjoint under the function $\lambda i', \sup_{x \in g(i')} f(x)$, meaning that for any distinct $i', j' \in s$, the suprema $\sup_{x \in g(i')} f(x)$ and $\sup_{x \in g(j')} f(x)$ are disjoint. 2. For each $i' \in s$, the finite set $g(i')$ is pairwise disjoint under $f$, meaning that for any distinct $x, y \in g(i')$, $f(x)$ and $f(y)$ are disjoint. Then the union $\bigcup_{i' \in s} g(i')$ is pairwise disjoint under $f$.

List.pairwise_of_coe_toFinset_pairwise theorem

(hl : (l.toFinset : Set α).Pairwise r) (hn : l.Nodup) : l.Pairwise r

Full source

theorem pairwise_of_coe_toFinset_pairwise (hl : (l.toFinset : Set α).Pairwise r) (hn : l.Nodup) :
    l.Pairwise r := by
  rw [coe_toFinset] at hl
  exact hn.pairwise_of_set_pairwise hl

Pairwise Relation on List from Pairwise Relation on Its Deduplicated Set

Informal description

Let $l$ be a list of elements of type $\alpha$ with no duplicates, and let $r$ be a binary relation on $\alpha$. If the set of elements in the finite set obtained from $l$ (by removing duplicates) is pairwise related by $r$, then the list $l$ itself is pairwise related by $r$.

List.pairwise_iff_coe_toFinset_pairwise theorem

(hn : l.Nodup) (hs : Symmetric r) : (l.toFinset : Set α).Pairwise r ↔ l.Pairwise r

Full source

theorem pairwise_iff_coe_toFinset_pairwise (hn : l.Nodup) (hs : Symmetric r) :
    (l.toFinset : Set α).Pairwise r ↔ l.Pairwise r := by
  letI : IsSymm α r := ⟨hs⟩
  rw [coe_toFinset, hn.pairwise_coe]

Equivalence of Pairwise Relations on List and Its Deduplicated Set under Symmetry and No Duplicates

Informal description

Let $l$ be a list of elements of type $\alpha$ with no duplicates, and let $r$ be a symmetric relation on $\alpha$. Then the set $\{a \mid a \in l\}$ is pairwise related by $r$ if and only if the list $l$ is pairwise related by $r$.

List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint theorem

 {α ι} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α}
  (hl : (l.toFinset : Set ι).PairwiseDisjoint f) (hn : l.Nodup) : l.Pairwise (_root_.Disjoint on f)

Full source

theorem pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α ι} [PartialOrder α] [OrderBot α]
    [DecidableEq ι] {l : List ι} {f : ι → α} (hl : (l.toFinset : Set ι).PairwiseDisjoint f)
    (hn : l.Nodup) : l.Pairwise (_root_.Disjoint_root_.Disjoint on f) :=
  pairwise_of_coe_toFinset_pairwise hl hn

Pairwise Disjointness of List Elements from Pairwise Disjointness of Their Set under a Function

Informal description

Let $\alpha$ be a partially ordered type with a bottom element $\bot$, and let $\iota$ be a type with decidable equality. Given a list $l$ of elements of type $\iota$ with no duplicates and a function $f \colon \iota \to \alpha$, if the set $\{i \mid i \in l\}$ is pairwise disjoint under $f$, then the list $l$ is pairwise disjoint under $f$ in the sense that for any two distinct elements $i, j \in l$, the images $f(i)$ and $f(j)$ are disjoint.

List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint theorem

 {α ι} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α} (hn : l.Nodup) :
  (l.toFinset : Set ι).PairwiseDisjoint f ↔ l.Pairwise (_root_.Disjoint on f)

Full source

theorem pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint {α ι} [PartialOrder α] [OrderBot α]
    [DecidableEq ι] {l : List ι} {f : ι → α} (hn : l.Nodup) :
    (l.toFinset : Set ι).PairwiseDisjoint f ↔ l.Pairwise (_root_.Disjoint on f) :=
  pairwise_iff_coe_toFinset_pairwise hn (symmetric_disjoint.comap f)

Equivalence of Pairwise Disjointness for List and Its Deduplicated Set under a Function

Informal description

Let $\alpha$ be a partially ordered type with a bottom element $\bot$, and let $\iota$ be a type with decidable equality. Given a list $l$ of elements of type $\iota$ with no duplicates and a function $f \colon \iota \to \alpha$, the following are equivalent: 1. The set $\{i \mid i \in l\}$ is pairwise disjoint under $f$, meaning that for any two distinct elements $i, j \in l$, the images $f(i)$ and $f(j)$ are disjoint. 2. The list $l$ is pairwise disjoint under $f$, meaning that for any two distinct elements $i, j \in l$, the images $f(i)$ and $f(j)$ are disjoint.