Documentation

Mathlib.Data.Set.Disjoint

Theorems about the Disjoint relation on Set. #

Set coercion to a type #

Disjointness #

source
theorem Set.disjoint_iff {α : Type u} {s t : Set α} :
Disjoint s t ↔ s ∩ t ⊆ ∅
source
theorem Set.disjoint_iff_inter_eq_empty {α : Type u} {s t : Set α} :
Disjoint s t ↔ s ∩ t = ∅
source
theorem Disjoint.inter_eq {α : Type u} {s t : Set α} :
Disjoint s t → s ∩ t = ∅
source
theorem Set.disjoint_left {α : Type u} {s t : Set α} :
Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
source
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.

source
theorem Set.disjoint_right {α : Type u} {s t : Set α} :
Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
source
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.

source
theorem Set.not_disjoint_iff {α : Type u} {s t : Set α} :
¬Disjoint s t ↔ ∃ x ∈ s, x ∈ t
source
theorem Set.not_disjoint_iff_nonempty_inter {α : Type u} {s t : Set α} :
¬Disjoint s t ↔ (s ∩ t).Nonempty
source
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.

source
theorem Set.disjoint_or_nonempty_inter {α : Type u} (s t : Set α) :
Disjoint s t ∨ (s ∩ t).Nonempty
source
theorem Set.disjoint_iff_forall_ne {α : Type u} {s t : Set α} :
Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
source
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.

source
theorem Set.disjoint_of_subset_left {α : Type u} {s t u : Set α} (h : s ⊆ u) (d : Disjoint u t) :
Disjoint s t
source
theorem Set.disjoint_of_subset_right {α : Type u} {s t u : Set α} (h : t ⊆ u) (d : Disjoint s u) :
Disjoint s t
source
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₁
source
@[simp]
theorem Set.disjoint_union_left {α : Type u} {s t u : Set α} :
Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
source
@[simp]
theorem Set.disjoint_union_right {α : Type u} {s t u : Set α} :
Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
source
@[simp]
theorem Set.disjoint_empty {α : Type u} (s : Set α) :
Disjoint s ∅
source
@[simp]
theorem Set.empty_disjoint {α : Type u} (s : Set α) :
Disjoint ∅ s
source
@[simp]
theorem Set.univ_disjoint {α : Type u} {s : Set α} :
Disjoint univ s ↔ s = ∅
source
@[simp]
theorem Set.disjoint_univ {α : Type u} {s : Set α} :
Disjoint s univ ↔ s = ∅
source
theorem Set.disjoint_sdiff_left {α : Type u} {s t : Set α} :
Disjoint (t \ s) s
source
theorem Set.disjoint_sdiff_right {α : Type u} {s t : Set α} :
Disjoint s (t \ s)
source
theorem Set.disjoint_sdiff_inter {α : Type u} {s t : Set α} :
Disjoint (s \ t) (s ∩ t)
source
theorem Set.subset_diff {α : Type u} {s t u : Set α} :
s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
source
theorem Set.disjoint_of_subset_iff_left_eq_empty {α : Type u} {s t : Set α} (h : s ⊆ t) :
Disjoint s t ↔ s = ∅

Lemmas about complement #

source
theorem Set.subset_compl_iff_disjoint_left {α : Type u} {s t : Set α} :
s ⊆ tᶜ ↔ Disjoint t s
source
theorem Set.subset_compl_iff_disjoint_right {α : Type u} {s t : Set α} :
s ⊆ tᶜ ↔ Disjoint s t
source
theorem Set.disjoint_compl_left_iff_subset {α : Type u} {s t : Set α} :
Disjoint sᶜ t ↔ t ⊆ s
source
theorem Set.disjoint_compl_right_iff_subset {α : Type u} {s t : Set α} :
Disjoint s tᶜ ↔ s ⊆ t
source
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.

source
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.

source
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.

source
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.

Disjoint sets #

source
theorem Disjoint.union_left {α : Type u_1} {s t u : Set α} (hs : Disjoint s u) (ht : Disjoint t u) :
Disjoint (s ∪ t) u
source
theorem Disjoint.union_right {α : Type u_1} {s t u : Set α} (ht : Disjoint s t) (hu : Disjoint s u) :
Disjoint s (t ∪ u)
source
theorem Disjoint.inter_left {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) :
Disjoint (s ∩ u) t
source
theorem Disjoint.inter_left' {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) :
Disjoint (u ∩ s) t
source
theorem Disjoint.inter_right {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) :
Disjoint s (t ∩ u)
source
theorem Disjoint.inter_right' {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) :
Disjoint s (u ∩ t)
source
theorem Disjoint.subset_left_of_subset_union {α : Type u_1} {s t u : Set α} (h : s ⊆ t ∪ u) (hac : Disjoint s u) :
s ⊆ t
source
theorem Disjoint.subset_right_of_subset_union {α : Type u_1} {s t u : Set α} (h : s ⊆ t ∪ u) (hab : Disjoint s t) :
s ⊆ u