Theorems about the Disjoint relation on Set.

Set coercion to a type

Disjointness

theorem Set.disjoint_iff {α : Type u} {s t : Set α} : Disjoint s t ↔ s ∩ t ⊆ ∅

theorem Set.disjoint_iff_inter_eq_empty {α : Type u} {s t : Set α} : Disjoint s t ↔ s ∩ t = ∅

theorem Disjoint.inter_eq {α : Type u} {s t : Set α} : Disjoint s t → s ∩ t = ∅

theorem Set.disjoint_left {α : Type u} {s t : Set α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t

theorem Disjoint.notMem_of_mem_left {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Alias of the forward direction of Set.disjoint_left.

@[deprecated Disjoint.notMem_of_mem_left (since := "2025-05-23")]

theorem Disjoint.not_mem_of_mem_left {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Alias of the forward direction of Set.disjoint_left.

---

Alias of the forward direction of Set.disjoint_left.

theorem Set.disjoint_right {α : Type u} {s t : Set α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

theorem Disjoint.notMem_of_mem_right {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Alias of the forward direction of Set.disjoint_right.

@[deprecated Disjoint.notMem_of_mem_right (since := "2025-05-23")]

theorem Disjoint.not_mem_of_mem_right {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Alias of the forward direction of Set.disjoint_right.

---

Alias of the forward direction of Set.disjoint_right.

theorem Set.not_disjoint_iff {α : Type u} {s t : Set α} : ¬Disjoint s t ↔ ∃ x ∈ s, x ∈ t

theorem Set.not_disjoint_iff_nonempty_inter {α : Type u} {s t : Set α} : ¬Disjoint s t ↔ (s ∩ t).Nonempty

theorem Set.Nonempty.not_disjoint {α : Type u} {s t : Set α} : (s ∩ t).Nonempty → ¬Disjoint s t

Alias of the reverse direction of Set.not_disjoint_iff_nonempty_inter.

theorem Set.disjoint_or_nonempty_inter {α : Type u} (s t : Set α) : Disjoint s t ∨ (s ∩ t).Nonempty

theorem Set.disjoint_iff_forall_ne {α : Type u} {s t : Set α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b

theorem Disjoint.ne_of_mem {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b

Alias of the forward direction of Set.disjoint_iff_forall_ne.

theorem Set.disjoint_of_subset_left {α : Type u} {s t u : Set α} (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t

theorem Set.disjoint_of_subset_right {α : Type u} {s t u : Set α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t

theorem Set.disjoint_of_subset {α : Type u} {s₁ s₂ t₁ t₂ : Set α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (h : Disjoint s₂ t₂) : Disjoint s₁ t₁

@[simp]

theorem Set.disjoint_union_left {α : Type u} {s t u : Set α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Set.disjoint_union_right {α : Type u} {s t u : Set α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

@[simp]

theorem Set.disjoint_empty {α : Type u} (s : Set α) : Disjoint s ∅

@[simp]

theorem Set.empty_disjoint {α : Type u} (s : Set α) : Disjoint ∅ s

@[simp]

theorem Set.univ_disjoint {α : Type u} {s : Set α} : Disjoint univ s ↔ s = ∅

@[simp]

theorem Set.disjoint_univ {α : Type u} {s : Set α} : Disjoint s univ ↔ s = ∅

theorem Set.disjoint_sdiff_left {α : Type u} {s t : Set α} : Disjoint (t \ s) s

theorem Set.disjoint_sdiff_right {α : Type u} {s t : Set α} : Disjoint s (t \ s)

theorem Set.disjoint_sdiff_inter {α : Type u} {s t : Set α} : Disjoint (s \ t) (s ∩ t)

theorem Set.subset_diff {α : Type u} {s t u : Set α} : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

theorem Set.disjoint_of_subset_iff_left_eq_empty {α : Type u} {s t : Set α} (h : s ⊆ t) : Disjoint s t ↔ s = ∅

Lemmas about complement

theorem Set.subset_compl_iff_disjoint_left {α : Type u} {s t : Set α} : s ⊆ tᶜ ↔ Disjoint t s

theorem Set.subset_compl_iff_disjoint_right {α : Type u} {s t : Set α} : s ⊆ tᶜ ↔ Disjoint s t

theorem Set.disjoint_compl_left_iff_subset {α : Type u} {s t : Set α} : Disjoint sᶜ t ↔ t ⊆ s

theorem Set.disjoint_compl_right_iff_subset {α : Type u} {s t : Set α} : Disjoint s tᶜ ↔ s ⊆ t

theorem Disjoint.subset_compl_right {α : Type u} {s t : Set α} : Disjoint s t → s ⊆ tᶜ

Alias of the reverse direction of Set.subset_compl_iff_disjoint_right.

theorem Disjoint.subset_compl_left {α : Type u} {s t : Set α} : Disjoint t s → s ⊆ tᶜ

Alias of the reverse direction of Set.subset_compl_iff_disjoint_left.

theorem HasSubset.Subset.disjoint_compl_left {α : Type u} {s t : Set α} : t ⊆ s → Disjoint sᶜ t

Alias of the reverse direction of Set.disjoint_compl_left_iff_subset.

theorem HasSubset.Subset.disjoint_compl_right {α : Type u} {s t : Set α} : s ⊆ t → Disjoint s tᶜ

Alias of the reverse direction of Set.disjoint_compl_right_iff_subset.

@[simp]

theorem Set.diff_ssubset_left_iff {α : Type u} {s t : Set α} : s \ t ⊂ s ↔ (s ∩ t).Nonempty

theorem HasSubset.Subset.diff_ssubset_of_nonempty {α : Type u} {s t : Set α} (hst : s ⊆ t) (hs : s.Nonempty) : t \ s ⊂ t

theorem Set.disjoint_range_iff {α : Type u} {β : Sort u_1} {γ : Sort u_2} {x : β → α} {y : γ → α} : Disjoint (range x) (range y) ↔ ∀ (i : β) (j : γ), x i ≠ y j

Disjoint sets

theorem Disjoint.union_left {α : Type u_1} {s t u : Set α} (hs : Disjoint s u) (ht : Disjoint t u) : Disjoint (s ∪ t) u

theorem Disjoint.union_right {α : Type u_1} {s t u : Set α} (ht : Disjoint s t) (hu : Disjoint s u) : Disjoint s (t ∪ u)

theorem Disjoint.inter_left {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint (s ∩ u) t

theorem Disjoint.inter_left' {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint (u ∩ s) t

theorem Disjoint.inter_right {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint s (t ∩ u)

theorem Disjoint.inter_right' {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint s (u ∩ t)

theorem Disjoint.subset_left_of_subset_union {α : Type u_1} {s t u : Set α} (h : s ⊆ t ∪ u) (hac : Disjoint s u) : s ⊆ t

theorem Disjoint.subset_right_of_subset_union {α : Type u_1} {s t u : Set α} (h : s ⊆ t ∪ u) (hab : Disjoint s t) : s ⊆ u