Mathlib.Data.Set.Disjoint

Set.disjoint_iff theorem

: Disjoint s t ↔ s ∩ t ⊆ ∅

Full source

protected theorem disjoint_iff : DisjointDisjoint s t ↔ s ∩ t ⊆ ∅ :=
  disjoint_iff_inf_le

Disjoint Sets Characterization via Subset of Empty Set

Informal description

Two sets $s$ and $t$ are disjoint if and only if their intersection is a subset of the empty set, i.e., $s \cap t \subseteq \emptyset$.

Set.disjoint_iff_inter_eq_empty theorem

: Disjoint s t ↔ s ∩ t = ∅

Full source

theorem disjoint_iff_inter_eq_empty : DisjointDisjoint s t ↔ s ∩ t = ∅ :=
  disjoint_iff

Disjoint Sets Characterization: $s \cap t = \emptyset$

Informal description

Two sets $s$ and $t$ are disjoint if and only if their intersection is the empty set, i.e., $s \cap t = \emptyset$.

Disjoint.inter_eq theorem

: Disjoint s t → s ∩ t = ∅

Full source

theorem _root_.Disjoint.inter_eq : Disjoint s t → s ∩ t = ∅ :=
  Disjoint.eq_bot

Intersection of Disjoint Sets is Empty

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, if $s$ and $t$ are disjoint, then their intersection is the empty set, i.e., $s \cap t = \emptyset$.

Set.disjoint_left theorem

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

Full source

theorem disjoint_left : DisjointDisjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t :=
  disjoint_iff_inf_le.trans <| forall_congr' fun _ => not_and

Left Disjointness Characterization: $s \cap t = \emptyset$ via Elements of $s$

Informal description

Two sets $s$ and $t$ are disjoint if and only if for every element $a$, if $a \in s$ then $a \notin t$.

Set.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 [disjoint_comm, disjoint_left]

Right Disjointness Characterization: $s \cap t = \emptyset$ via Elements of $t$

Informal description

Two sets $s$ and $t$ are disjoint if and only if for every element $a$, if $a \in t$ then $a \notin s$.

Set.not_disjoint_iff theorem

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

Full source

lemma not_disjoint_iff : ¬Disjoint s t¬Disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t :=
  Set.disjoint_iff.not.trans <| not_forall.trans <| exists_congr fun _ ↦ not_not

Non-Disjoint Sets Have Common Element

Informal description

Two sets $s$ and $t$ are not disjoint if and only if there exists an element $x$ such that $x \in s$ and $x \in t$.

Set.not_disjoint_iff_nonempty_inter theorem

: ¬Disjoint s t ↔ (s ∩ t).Nonempty

Full source

lemma not_disjoint_iff_nonempty_inter : ¬ Disjoint s t¬ Disjoint s t ↔ (s ∩ t).Nonempty := not_disjoint_iff

Non-Disjointness Equivalent to Nonempty Intersection

Informal description

Two sets $s$ and $t$ are not disjoint if and only if their intersection $s \cap t$ is nonempty.

Set.disjoint_or_nonempty_inter theorem

(s t : Set α) : Disjoint s t ∨ (s ∩ t).Nonempty

Full source

lemma disjoint_or_nonempty_inter (s t : Set α) : DisjointDisjoint s t ∨ (s ∩ t).Nonempty :=
  (em _).imp_right not_disjoint_iff_nonempty_inter.1

Disjointness or Nonempty Intersection of Sets

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, either $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$) or their intersection is nonempty (i.e., there exists an element $x \in s \cap t$).

Set.disjoint_iff_forall_ne theorem

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

Full source

lemma disjoint_iff_forall_ne : DisjointDisjoint s t ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ t → a ≠ b := by
  simp only [Ne, disjoint_left, @imp_not_comm _ (_ = _), forall_eq']

Characterization of Disjoint Sets via Distinct Elements

Informal description

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

Set.disjoint_of_subset_left theorem

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

Full source

lemma disjoint_of_subset_left (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t := d.mono_left h

Disjointness Preserved Under Subset Inclusion on the Left

Informal description

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

Set.disjoint_of_subset_right theorem

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

Full source

lemma disjoint_of_subset_right (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t := d.mono_right h

Disjointness Preserved Under Subset Inclusion on the Right

Informal description

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

Set.disjoint_of_subset theorem

(hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (h : Disjoint s₂ t₂) : Disjoint s₁ t₁

Full source

lemma disjoint_of_subset (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (h : Disjoint s₂ t₂) : Disjoint s₁ t₁ :=
  h.mono hs ht

Disjointness Preserved Under Subset Inclusion

Informal description

For any sets $s₁, s₂, t₁, t₂$ over a type $\alpha$, if $s₁ \subseteq s₂$ and $t₁ \subseteq t₂$, and $s₂$ and $t₂$ are disjoint, then $s₁$ and $t₁$ are also disjoint.

Set.disjoint_union_left theorem

: Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Full source

@[simp]
lemma disjoint_union_left : DisjointDisjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u := disjoint_sup_left

Disjointness of Union: $s \cup t \mathbin{\text{disjoint}} u \leftrightarrow s \mathbin{\text{disjoint}} u \land t \mathbin{\text{disjoint}} u$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the union $s \cup t$ is disjoint from $u$ if and only if both $s$ is disjoint from $u$ and $t$ is disjoint from $u$.

Set.disjoint_union_right theorem

: Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

Full source

@[simp]
lemma disjoint_union_right : DisjointDisjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u := disjoint_sup_right

Disjointness with Union: $s \mathbin{\text{disjoint}} (t \cup u) \leftrightarrow s \mathbin{\text{disjoint}} t \land s \mathbin{\text{disjoint}} u$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the set $s$ is disjoint from the union $t \cup u$ if and only if $s$ is disjoint from $t$ and $s$ is disjoint from $u$. In other words, $s \cap (t \cup u) = \emptyset \leftrightarrow s \cap t = \emptyset \land s \cap u = \emptyset$.

Set.disjoint_empty theorem

(s : Set α) : Disjoint s ∅

Full source

@[simp] lemma disjoint_empty (s : Set α) : Disjoint s ∅ := disjoint_bot_right

Any Set is Disjoint from the Empty Set

Informal description

For any set $s$ over a type $\alpha$, the set $s$ is disjoint from the empty set $\emptyset$.

Set.empty_disjoint theorem

(s : Set α) : Disjoint ∅ s

Full source

@[simp] lemma empty_disjoint (s : Set α) : Disjoint ∅ s := disjoint_bot_left

Empty Set is Disjoint from Any Set

Informal description

For any set $s$ over a type $\alpha$, the empty set $\emptyset$ is disjoint from $s$.

Set.univ_disjoint theorem

: Disjoint univ s ↔ s = ∅

Full source

@[simp] lemma univ_disjoint : DisjointDisjoint univ s ↔ s = ∅ := top_disjoint

Universal Set Disjointness Criterion: $\text{univ} \cap s = \emptyset \leftrightarrow s = \emptyset$

Informal description

For any set $s$ over a type $\alpha$, the universal set is disjoint from $s$ if and only if $s$ is the empty set. In other words, $\text{univ} \cap s = \emptyset \leftrightarrow s = \emptyset$.

Set.disjoint_univ theorem

: Disjoint s univ ↔ s = ∅

Full source

@[simp] lemma disjoint_univ : DisjointDisjoint s univ ↔ s = ∅ := disjoint_top

Disjointness with Universal Set Characterizes the Empty Set

Informal description

For any set $s$ in a type $\alpha$, the set $s$ is disjoint from the universal set (the set containing all elements of $\alpha$) if and only if $s$ is the empty set. In other words, $s \cap \text{univ} = \emptyset \leftrightarrow s = \emptyset$.

Set.disjoint_sdiff_left theorem

: Disjoint (t \ s) s

Full source

lemma disjoint_sdiff_left : Disjoint (t \ s) s := disjoint_sdiff_self_left

Disjointness of Set Difference and Original Set

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the set difference $t \setminus s$ is disjoint from $s$.

Set.disjoint_sdiff_right theorem

: Disjoint s (t \ s)

Full source

lemma disjoint_sdiff_right : Disjoint s (t \ s) := disjoint_sdiff_self_right

Disjointness of a Set with Its Relative Complement

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the sets $s$ and $t \setminus s$ are disjoint, i.e., $s \cap (t \setminus s) = \emptyset$.

Set.disjoint_sdiff_inter theorem

: Disjoint (s \ t) (s ∩ t)

Full source

theorem disjoint_sdiff_inter : Disjoint (s \ t) (s ∩ t) :=
  disjoint_of_subset_right inter_subset_right disjoint_sdiff_left

Disjointness of Set Difference and Intersection: $(s \setminus t) \cap (s \cap t) = \emptyset$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the set difference $s \setminus t$ is disjoint from the intersection $s \cap t$.

Set.subset_diff theorem

: s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

Full source

lemma subset_diff : s ⊆ t \ us ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u := le_iff_subset.symm.trans le_sdiff

Subset Characterization via Set Difference and Disjointness

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the subset relation $s \subseteq t \setminus u$ holds if and only if $s$ is a subset of $t$ and $s$ is disjoint from $u$.

Set.disjoint_of_subset_iff_left_eq_empty theorem

(h : s ⊆ t) : Disjoint s t ↔ s = ∅

Full source

theorem disjoint_of_subset_iff_left_eq_empty (h : s ⊆ t) :
    DisjointDisjoint s t ↔ s = ∅ :=
  disjoint_of_le_iff_left_eq_bot h

Disjointness of Subset and Superset Implies Subset is Empty

Informal description

For any sets $s$ and $t$ such that $s \subseteq t$, the sets $s$ and $t$ are disjoint if and only if $s$ is the empty set, i.e., $s = \emptyset$.

Set.subset_compl_iff_disjoint_left theorem

: s ⊆ tᶜ ↔ Disjoint t s

Full source

theorem subset_compl_iff_disjoint_left : s ⊆ tᶜs ⊆ tᶜ ↔ Disjoint t s :=
  @le_compl_iff_disjoint_left (Set α) _ _ _

Subset of Complement Characterizes Disjointness (Symmetric Form): $s \subseteq t^c \leftrightarrow t \cap s = \emptyset$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the subset relation $s \subseteq t^c$ holds if and only if $t$ and $s$ are disjoint (i.e., $t \cap s = \emptyset$).

Set.subset_compl_iff_disjoint_right theorem

: s ⊆ tᶜ ↔ Disjoint s t

Full source

theorem subset_compl_iff_disjoint_right : s ⊆ tᶜs ⊆ tᶜ ↔ Disjoint s t :=
  @le_compl_iff_disjoint_right (Set α) _ _ _

Subset of Complement Characterizes Disjointness: $s \subseteq t^c \leftrightarrow s \cap t = \emptyset$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the subset relation $s \subseteq t^c$ holds if and only if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$).

Set.disjoint_compl_left_iff_subset theorem

: Disjoint sᶜ t ↔ t ⊆ s

Full source

theorem disjoint_compl_left_iff_subset : DisjointDisjoint sᶜ t ↔ t ⊆ s :=
  disjoint_compl_left_iff

Disjointness of Complement and Subset Relation: $s^c \cap t = \emptyset \iff t \subseteq s$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the complement of $s$ is disjoint from $t$ if and only if $t$ is a subset of $s$. In symbols: \[ s^c \cap t = \emptyset \iff t \subseteq s. \]

Set.disjoint_compl_right_iff_subset theorem

: Disjoint s tᶜ ↔ s ⊆ t

Full source

theorem disjoint_compl_right_iff_subset : DisjointDisjoint s tᶜ ↔ s ⊆ t :=
  disjoint_compl_right_iff

Disjointness with Complement is Equivalent to Subset: $s \cap t^c = \emptyset \leftrightarrow s \subseteq t$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the sets $s$ and the complement of $t$ are disjoint if and only if $s$ is a subset of $t$. In symbols, $s \cap t^c = \emptyset \leftrightarrow s \subseteq t$.

Set.diff_ssubset_left_iff theorem

: s \ t ⊂ s ↔ (s ∩ t).Nonempty

Full source

@[simp]
theorem diff_ssubset_left_iff : s \ ts \ t ⊂ ss \ t ⊂ s ↔ (s ∩ t).Nonempty :=
  sdiff_lt_left.trans <| by rw [not_disjoint_iff_nonempty_inter, inter_comm]

Proper Subset Condition for Set Difference: $s \setminus t \subset s \leftrightarrow s \cap t \neq \emptyset$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the set difference $s \setminus t$ is a proper subset of $s$ if and only if the intersection $s \cap t$ is nonempty.

HasSubset.Subset.diff_ssubset_of_nonempty theorem

(hst : s ⊆ t) (hs : s.Nonempty) : t \ s ⊂ t

Full source

theorem _root_.HasSubset.Subset.diff_ssubset_of_nonempty (hst : s ⊆ t) (hs : s.Nonempty) :
    t \ st \ s ⊂ t := by
  simpa [inter_eq_self_of_subset_right hst]

Proper subset relation for nonempty subset differences

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $s$ is a subset of $t$ and $s$ is nonempty, then the set difference $t \setminus s$ is a proper subset of $t$.

Disjoint.union_left theorem

(hs : Disjoint s u) (ht : Disjoint t u) : Disjoint (s ∪ t) u

Full source

theorem union_left (hs : Disjoint s u) (ht : Disjoint t u) : Disjoint (s ∪ t) u :=
  hs.sup_left ht

Disjointness is preserved under left union

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if $s$ is disjoint from $u$ and $t$ is disjoint from $u$, then the union $s \cup t$ is also disjoint from $u$.

Disjoint.union_right theorem

(ht : Disjoint s t) (hu : Disjoint s u) : Disjoint s (t ∪ u)

Full source

theorem union_right (ht : Disjoint s t) (hu : Disjoint s u) : Disjoint s (t ∪ u) :=
  ht.sup_right hu

Disjointness is Preserved Under Union in the Second Argument

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if $s$ is disjoint from $t$ and $s$ is disjoint from $u$, then $s$ is disjoint from the union $t \cup u$.

Disjoint.inter_left theorem

(u : Set α) (h : Disjoint s t) : Disjoint (s ∩ u) t

Full source

theorem inter_left (u : Set α) (h : Disjoint s t) : Disjoint (s ∩ u) t :=
  h.inf_left _

Left Intersection Preserves Disjointness

Informal description

For any set $u$ in a type $\alpha$, if sets $s$ and $t$ are disjoint, then the intersection of $s$ with $u$ is also disjoint with $t$.

Disjoint.inter_left' theorem

(u : Set α) (h : Disjoint s t) : Disjoint (u ∩ s) t

Full source

theorem inter_left' (u : Set α) (h : Disjoint s t) : Disjoint (u ∩ s) t :=
  h.inf_left' _

Intersection Preserves Disjointness on the Left

Informal description

For any set $u$ in a type $\alpha$, if sets $s$ and $t$ are disjoint, then the intersection of $u$ and $s$ is also disjoint with $t$.

Disjoint.inter_right theorem

(u : Set α) (h : Disjoint s t) : Disjoint s (t ∩ u)

Full source

theorem inter_right (u : Set α) (h : Disjoint s t) : Disjoint s (t ∩ u) :=
  h.inf_right _

Disjointness Preservation under Right Intersection

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if $s$ and $t$ are disjoint, then $s$ is also disjoint with the intersection $t \cap u$.

Disjoint.inter_right' theorem

(u : Set α) (h : Disjoint s t) : Disjoint s (u ∩ t)

Full source

theorem inter_right' (u : Set α) (h : Disjoint s t) : Disjoint s (u ∩ t) :=
  h.inf_right' _

Disjointness Preserved Under Right Intersection

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, if $s$ and $t$ are disjoint, then $s$ is also disjoint with the intersection $u \cap t$.

Disjoint.subset_left_of_subset_union theorem

(h : s ⊆ t ∪ u) (hac : Disjoint s u) : s ⊆ t

Full source

theorem subset_left_of_subset_union (h : s ⊆ t ∪ u) (hac : Disjoint s u) : s ⊆ t :=
  hac.left_le_of_le_sup_right h

Subset from Union when Disjoint from One Component

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, if $s$ is a subset of the union $t \cup u$ and $s$ is disjoint from $u$, then $s$ is a subset of $t$.

Disjoint.subset_right_of_subset_union theorem

(h : s ⊆ t ∪ u) (hab : Disjoint s t) : s ⊆ u

Full source

theorem subset_right_of_subset_union (h : s ⊆ t ∪ u) (hab : Disjoint s t) : s ⊆ u :=
  hab.left_le_of_le_sup_left h

Disjointness Implies Subset of Remaining Component in Union

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, if $s$ is a subset of the union $t \cup u$ and $s$ is disjoint from $t$, then $s$ is a subset of $u$.