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.

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.

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

theorem Set.mem_union_of_disjoint {α : Type u_1} {s t : Set α} (h : Disjoint s t) {x : α} : x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)