Mathlib.Data.Finset.Disjoint

Finset.disjoint_left theorem

: Disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t

Full source

theorem disjoint_left : DisjointDisjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t :=
  ⟨fun h a hs ht => not_mem_empty a <|
    singleton_subset_iff.mp (h (singleton_subset_iff.mpr hs) (singleton_subset_iff.mpr ht)),
    fun h _ hs ht _ ha => (h (hs ha) (ht ha)).elim⟩

Disjointness Criterion for Finite Sets via Left Membership

Informal description

Two finite sets $s$ and $t$ are disjoint if and only if for every element $a$ in $s$, $a$ does not belong to $t$.

Finset.disjoint_right theorem

: Disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s

Full source

theorem disjoint_right : DisjointDisjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s := by
  rw [_root_.disjoint_comm, disjoint_left]

Disjointness Criterion for Finite Sets via Right Membership

Informal description

Two finite sets $s$ and $t$ are disjoint if and only if for every element $a$ in $t$, $a$ does not belong to $s$.

Finset.disjoint_iff_ne theorem

: Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Full source

theorem disjoint_iff_ne : DisjointDisjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b := by
  simp only [disjoint_left, imp_not_comm, forall_eq']

Characterization of Disjoint Finite Sets via Distinct Elements

Informal description

Two finite sets $s$ and $t$ are disjoint if and only if for every element $a \in s$ and every element $b \in t$, we have $a \neq b$.

Finset.disjoint_val theorem

: Disjoint s.1 t.1 ↔ Disjoint s t

Full source

@[simp]
theorem disjoint_val : DisjointDisjoint s.1 t.1 ↔ Disjoint s t :=
  Multiset.disjoint_left.trans disjoint_left.symm

Disjointness of Finite Sets via Underlying Multisets

Informal description

For two finite sets $s$ and $t$ of type $\alpha$, the underlying multisets of $s$ and $t$ are disjoint if and only if the sets $s$ and $t$ themselves are disjoint.

Disjoint.forall_ne_finset theorem

(h : Disjoint s t) (ha : a ∈ s) (hb : b ∈ t) : a ≠ b

Full source

theorem _root_.Disjoint.forall_ne_finset (h : Disjoint s t) (ha : a ∈ s) (hb : b ∈ t) : a ≠ b :=
  disjoint_iff_ne.1 h _ ha _ hb

Disjoint Finite Sets Have Distinct Elements

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, if $s$ and $t$ are disjoint, then for any element $a \in s$ and any element $b \in t$, we have $a \neq b$.

Finset.not_disjoint_iff theorem

: ¬Disjoint s t ↔ ∃ a, a ∈ s ∧ a ∈ t

Full source

theorem not_disjoint_iff : ¬Disjoint s t¬Disjoint s t ↔ ∃ a, a ∈ s ∧ a ∈ t :=
  disjoint_left.not.trans <| not_forall.trans <| exists_congr fun _ => by
    rw [Classical.not_imp, not_not]

Non-disjoint Finite Sets Have Common Element

Informal description

Two finite sets $s$ and $t$ are not disjoint if and only if there exists an element $a$ such that $a$ belongs to both $s$ and $t$.

Finset.disjoint_of_subset_left theorem

(h : s ⊆ u) (d : Disjoint u t) : Disjoint s t

Full source

theorem disjoint_of_subset_left (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t :=
  disjoint_left.2 fun _x m₁ => (disjoint_left.1 d) (h m₁)

Disjointness Preservation under Subset Inclusion

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, if $s$ is a subset of $u$ and $u$ is disjoint with $t$, then $s$ is also disjoint with $t$.

Finset.disjoint_of_subset_right theorem

(h : t ⊆ u) (d : Disjoint s u) : Disjoint s t

Full source

theorem disjoint_of_subset_right (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t :=
  disjoint_right.2 fun _x m₁ => (disjoint_right.1 d) (h m₁)

Disjointness Preservation under Right Subset Inclusion

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, if $t$ is a subset of $u$ and $s$ is disjoint with $u$, then $s$ is also disjoint with $t$.

Finset.disjoint_empty_left theorem

(s : Finset α) : Disjoint ∅ s

Full source

@[simp]
theorem disjoint_empty_left (s : Finset α) : Disjoint ∅ s :=
  disjoint_bot_left

Empty Set is Disjoint with Any Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the empty set $\emptyset$ is disjoint with $s$.

Finset.disjoint_empty_right theorem

(s : Finset α) : Disjoint s ∅

Full source

@[simp]
theorem disjoint_empty_right (s : Finset α) : Disjoint s ∅ :=
  disjoint_bot_right

Any Finite Set is Disjoint with the Empty Set

Informal description

For any finite set $s$ of type $\alpha$, $s$ is disjoint with the empty set $\emptyset$.

Finset.disjoint_singleton_left theorem

: Disjoint (singleton a) s ↔ a ∉ s

Full source

@[simp]
theorem disjoint_singleton_left : DisjointDisjoint (singleton a) s ↔ a ∉ s := by
  simp only [disjoint_left, mem_singleton, forall_eq]

Disjointness of Singleton and Finite Set: $\{a\} \cap s = \emptyset \leftrightarrow a \notin s$

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the singleton set $\{a\}$ is disjoint from $s$ if and only if $a$ is not an element of $s$.

Finset.disjoint_singleton_right theorem

: Disjoint s (singleton a) ↔ a ∉ s

Full source

@[simp]
theorem disjoint_singleton_right : DisjointDisjoint s (singleton a) ↔ a ∉ s :=
  disjoint_comm.trans disjoint_singleton_left

Disjointness of Finite Set and Singleton: $s \cap \{a\} = \emptyset \leftrightarrow a \notin s$

Informal description

For any finite set $s$ of type $\alpha$ and any element $a$ of type $\alpha$, the set $s$ is disjoint from the singleton set $\{a\}$ if and only if $a$ does not belong to $s$, i.e., $s \cap \{a\} = \emptyset \leftrightarrow a \notin s$.

Finset.disjoint_singleton theorem

: Disjoint ({ a } : Finset α) { b } ↔ a ≠ b

Full source

theorem disjoint_singleton : DisjointDisjoint ({a} : Finset α) {b} ↔ a ≠ b := by
  rw [disjoint_singleton_left, mem_singleton]

Disjointness of Singletons: $\{a\} \cap \{b\} = \emptyset \leftrightarrow a \neq b$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the singleton sets $\{a\}$ and $\{b\}$ are disjoint if and only if $a \neq b$.

Finset.disjoint_self_iff_empty theorem

(s : Finset α) : Disjoint s s ↔ s = ∅

Full source

theorem disjoint_self_iff_empty (s : Finset α) : DisjointDisjoint s s ↔ s = ∅ :=
  disjoint_self

Self-Disjointness of Finite Sets Equals Emptiness

Informal description

For any finite set $s$ of type $\alpha$, the set $s$ is disjoint from itself if and only if $s$ is the empty set, i.e., $s \cap s = \emptyset \Leftrightarrow s = \emptyset$.

Finset.disjoint_coe theorem

: Disjoint (s : Set α) t ↔ Disjoint s t

Full source

@[simp, norm_cast]
theorem disjoint_coe : DisjointDisjoint (s : Set α) t ↔ Disjoint s t := by
  simp only [Finset.disjoint_left, Set.disjoint_left, mem_coe]

Disjointness of Finite Sets via Set Embedding

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, the sets are disjoint (i.e., $s \cap t = \emptyset$) if and only if their corresponding sets under the canonical embedding into the type of all sets over $\alpha$ are disjoint.

Finset.pairwiseDisjoint_coe theorem

 {ι : Type*} {s : Set ι} {f : ι → Finset α} : s.PairwiseDisjoint (fun i => f i : ι → Set α) ↔ s.PairwiseDisjoint f

Full source

@[simp, norm_cast]
theorem pairwiseDisjoint_coe {ι : Type*} {s : Set ι} {f : ι → Finset α} :
    s.PairwiseDisjoint (fun i => f i : ι → Set α) ↔ s.PairwiseDisjoint f :=
  forall₅_congr fun _ _ _ _ _ => disjoint_coe

Equivalence of Pairwise Disjointness for Finite Sets and Their Set Embeddings

Informal description

For any type $\iota$ and any set $s \subseteq \iota$, and for any function $f \colon \iota \to \text{Finset}\ \alpha$, the set $s$ is pairwise disjoint with respect to the function $f$ (viewed as mapping to finite sets) if and only if $s$ is pairwise disjoint with respect to the function $\lambda i, (f i : \text{Set}\ \alpha)$ (viewed as mapping to sets). In other words, for any two distinct elements $i, j \in s$, the finite sets $f(i)$ and $f(j)$ are disjoint if and only if their corresponding sets (under the canonical embedding) are disjoint.

Finset.decidableDisjoint instance

(U V : Finset α) : Decidable (Disjoint U V)

Full source

instance decidableDisjoint (U V : Finset α) : Decidable (Disjoint U V) :=
  decidable_of_iff _ disjoint_left.symm

Decidability of Disjointness for Finite Sets

Informal description

For any two finite sets $U$ and $V$ of a type $\alpha$, the property of being disjoint (i.e., having empty intersection) is decidable.

Finset.disjUnion definition

(s t : Finset α) (h : Disjoint s t) : Finset α

Full source

/-- `disjUnion s t h` is the set such that `a ∈ disjUnion s t h` iff `a ∈ s` or `a ∈ t`.
It is the same as `s ∪ t`, but it does not require decidable equality on the type. The hypothesis
ensures that the sets are disjoint. -/
def disjUnion (s t : Finset α) (h : Disjoint s t) : Finset α :=
  ⟨s.1 + t.1, Multiset.nodup_add.2 ⟨s.2, t.2, disjoint_val.2 h⟩⟩

Disjoint union of finite sets

Informal description

Given two finite sets $s$ and $t$ of type $\alpha$ and a proof $h$ that they are disjoint, the operation $\text{disjUnion}$ constructs their union as a finite set. An element $a$ belongs to $\text{disjUnion}\ s\ t\ h$ if and only if $a \in s$ or $a \in t$. This operation does not require decidable equality on $\alpha$ and ensures that the union is well-defined under the disjointness condition.

Finset.mem_disjUnion theorem

{α s t h a} : a ∈ @disjUnion α s t h ↔ a ∈ s ∨ a ∈ t

Full source

@[simp]
theorem mem_disjUnion {α s t h a} : a ∈ @disjUnion α s t ha ∈ @disjUnion α s t h ↔ a ∈ s ∨ a ∈ t := by
  rcases s with ⟨⟨s⟩⟩; rcases t with ⟨⟨t⟩⟩; apply List.mem_append

Membership in Disjoint Union of Finite Sets

Informal description

For any element $a$ of type $\alpha$ and any two finite sets $s$ and $t$ of $\alpha$ that are disjoint (i.e., $s \cap t = \emptyset$), the element $a$ belongs to the disjoint union $\text{disjUnion}\ s\ t\ h$ if and only if $a \in s$ or $a \in t$.

Finset.coe_disjUnion theorem

{s t : Finset α} (h : Disjoint s t) : (disjUnion s t h : Set α) = (s : Set α) ∪ t

Full source

@[simp, norm_cast]
theorem coe_disjUnion {s t : Finset α} (h : Disjoint s t) :
    (disjUnion s t h : Set α) = (s : Set α) ∪ t :=
  Set.ext <| by simp

Underlying Set of Disjoint Union Equals Union of Underlying Sets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$ that are disjoint (i.e., $s \cap t = \emptyset$), the underlying set of their disjoint union $\text{disjUnion}\ s\ t\ h$ is equal to the union of the underlying sets of $s$ and $t$, i.e., $(\text{disjUnion}\ s\ t\ h : \text{Set}\ \alpha) = (s : \text{Set}\ \alpha) \cup t$.

Finset.disjUnion_comm theorem

(s t : Finset α) (h : Disjoint s t) : disjUnion s t h = disjUnion t s h.symm

Full source

theorem disjUnion_comm (s t : Finset α) (h : Disjoint s t) :
    disjUnion s t h = disjUnion t s h.symm :=
  eq_of_veq <| Multiset.add_comm _ _

Commutativity of Disjoint Union for Finite Sets: $\text{disjUnion}\ s\ t\ h = \text{disjUnion}\ t\ s\ h.\text{symm}$

Informal description

For any two disjoint finite sets $s$ and $t$ of type $\alpha$, the disjoint union $\text{disjUnion}\ s\ t\ h$ is equal to $\text{disjUnion}\ t\ s\ h.\text{symm}$, where $h.\text{symm}$ is the symmetric version of the disjointness proof $h$.

Finset.singleton_disjUnion theorem

(a : α) (t : Finset α) (h : Disjoint { a } t) : disjUnion { a } t h = cons a t (disjoint_singleton_left.mp h)

Full source

theorem singleton_disjUnion (a : α) (t : Finset α) (h : Disjoint {a} t) :
    disjUnion {a} t h = cons a t (disjoint_singleton_left.mp h) :=
  eq_of_veq <| Multiset.singleton_add _ _

Disjoint Union of Singleton and Finite Set: $\{a\} \sqcup t = a \mathbin{::} t$ when $\{a\} \cap t = \emptyset$

Informal description

For any element $a$ of type $\alpha$ and any finite set $t$ of type $\alpha$, if the singleton set $\{a\}$ is disjoint from $t$, then the disjoint union of $\{a\}$ and $t$ is equal to the finite set obtained by inserting $a$ into $t$.

Finset.disjUnion_singleton theorem

(s : Finset α) (a : α) (h : Disjoint s { a }) : disjUnion s { a } h = cons a s (disjoint_singleton_right.mp h)

Full source

theorem disjUnion_singleton (s : Finset α) (a : α) (h : Disjoint s {a}) :
    disjUnion s {a} h = cons a s (disjoint_singleton_right.mp h) := by
  rw [disjUnion_comm, singleton_disjUnion]

Disjoint Union of Finite Set and Singleton: $s \sqcup \{a\} = a \mathbin{::} s$ when $s \cap \{a\} = \emptyset$

Informal description

For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, if $s$ is disjoint from the singleton set $\{a\}$, then the disjoint union of $s$ and $\{a\}$ is equal to the finite set obtained by inserting $a$ into $s$.

Finset.disjoint_insert_left theorem

: Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Full source

@[simp]
theorem disjoint_insert_left : DisjointDisjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t := by
  simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]

Disjointness Condition for Insertion on the Left: $\{a\} \cup s \cap t = \emptyset \leftrightarrow a \notin t \land s \cap t = \emptyset$

Informal description

For any finite sets $s$ and $t$ of type $\alpha$ and any element $a \in \alpha$, the set $\{a\} \cup s$ is disjoint from $t$ if and only if $a$ is not in $t$ and $s$ is disjoint from $t$.

Finset.disjoint_insert_right theorem

: Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t

Full source

@[simp]
theorem disjoint_insert_right : DisjointDisjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t :=
  disjoint_comm.trans <| by rw [disjoint_insert_left, _root_.disjoint_comm]

Disjointness Condition for Insertion on the Right: $s \cap (\{a\} \cup t) = \emptyset \leftrightarrow a \notin s \land s \cap t = \emptyset$

Informal description

For any finite sets $s$ and $t$ of type $\alpha$ and any element $a \in \alpha$, the set $s$ is disjoint from $\{a\} \cup t$ if and only if $a$ is not in $s$ and $s$ is disjoint from $t$.

Multiset.disjoint_toFinset theorem

{m1 m2 : Multiset α} : _root_.Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2

Full source

@[simp]
theorem disjoint_toFinset {m1 m2 : Multiset α} :
    _root_.Disjoint_root_.Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2 := by
  simp [disjoint_left, Finset.disjoint_left]

Disjointness of Multiset-to-Finset Conversion: $m_1.toFinset \cap m_2.toFinset = \emptyset \leftrightarrow m_1 \cap m_2 = \emptyset$

Informal description

For any two multisets $m_1$ and $m_2$ over a type $\alpha$, the finite sets obtained from converting $m_1$ and $m_2$ to finsets are disjoint if and only if the multisets $m_1$ and $m_2$ themselves are disjoint. In other words, $m_1.toFinset \cap m_2.toFinset = \emptyset \leftrightarrow m_1 \cap m_2 = \emptyset$.

List.disjoint_toFinset_iff_disjoint theorem

: _root_.Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l'

Full source

@[simp]
theorem disjoint_toFinset_iff_disjoint : _root_.Disjoint_root_.Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l' :=
  Multiset.disjoint_toFinset.trans (Multiset.coe_disjoint _ _)

Disjointness of List-to-Finset Conversion: $l.toFinset \cap l'.toFinset = \emptyset \leftrightarrow l \cap l' = \emptyset$

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the finite sets obtained from converting $l$ and $l'$ to finsets are disjoint if and only if the lists $l$ and $l'$ themselves are disjoint (i.e., they have no common elements).

Mathlib.Data.Finset.Disjoint

Main declarations

Tags