Documentation

Mathlib.Data.Finset.Disjoint

Disjoint finite sets #

Main declarations #

Tags #

finite sets, finset

disjoint #

source
theorem Finset.disjoint_left {α : Type u_1} {s t : Finset α} :
Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
source
theorem Disjoint.notMem_of_mem_left_finset {α : Type u_1} {s t : Finset α} :
Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Alias of the forward direction of Finset.disjoint_left.

source
@[deprecated Disjoint.notMem_of_mem_left_finset (since := "2025-05-23")]
theorem Disjoint.not_mem_of_mem_left_finset {α : Type u_1} {s t : Finset α} :
Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Alias of the forward direction of Finset.disjoint_left.

Alias of the forward direction of Finset.disjoint_left.

source
theorem Finset.disjoint_right {α : Type u_1} {s t : Finset α} :
Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
source
theorem Disjoint.notMem_of_mem_right_finset {α : Type u_1} {s t : Finset α} :
Disjoint s t → ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Alias of the forward direction of Finset.disjoint_right.

source
@[deprecated Disjoint.notMem_of_mem_right_finset (since := "2025-05-23")]
theorem Disjoint.not_mem_of_mem_right_finset {α : Type u_1} {s t : Finset α} :
Disjoint s t → ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Alias of the forward direction of Finset.disjoint_right.

Alias of the forward direction of Finset.disjoint_right.

source
theorem Finset.disjoint_iff_ne {α : Type u_1} {s t : Finset α} :
Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
source
@[simp]
theorem Finset.disjoint_val {α : Type u_1} {s t : Finset α} :
Disjoint s.val t.val ↔ Disjoint s t
source
theorem Disjoint.forall_ne_finset {α : Type u_1} {s t : Finset α} {a b : α} (h : Disjoint s t) (ha : a ∈ s) (hb : b ∈ t) :
a ≠ b
source
theorem Finset.not_disjoint_iff {α : Type u_1} {s t : Finset α} :
¬Disjoint s t ↔ ∃ a ∈ s, a ∈ t
source
theorem Finset.disjoint_of_subset_left {α : Type u_1} {s t u : Finset α} (h : s ⊆ u) (d : Disjoint u t) :
Disjoint s t
source
theorem Finset.disjoint_of_subset_right {α : Type u_1} {s t u : Finset α} (h : t ⊆ u) (d : Disjoint s u) :
Disjoint s t
source
@[simp]
theorem Finset.disjoint_empty_left {α : Type u_1} (s : Finset α) :
Disjoint ∅ s
source
@[simp]
theorem Finset.disjoint_empty_right {α : Type u_1} (s : Finset α) :
Disjoint s ∅
source
@[simp]
theorem Finset.disjoint_singleton_left {α : Type u_1} {s : Finset α} {a : α} :
Disjoint {a} s ↔ a ∉ s
source
@[simp]
theorem Finset.disjoint_singleton_right {α : Type u_1} {s : Finset α} {a : α} :
Disjoint s {a} ↔ a ∉ s
source
theorem Finset.disjoint_singleton {α : Type u_1} {a b : α} :
Disjoint {a} {b} ↔ a ≠ b
source
theorem Finset.disjoint_self_iff_empty {α : Type u_1} (s : Finset α) :
Disjoint s s ↔ s = ∅
source
@[simp]
theorem Finset.disjoint_coe {α : Type u_1} {s t : Finset α} :
Disjoint ↑s ↑t ↔ Disjoint s t
source
@[simp]
theorem Finset.pairwiseDisjoint_coe {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ι → Finset α} :
(s.PairwiseDisjoint fun (i : ι) => ↑(f i)) ↔ s.PairwiseDisjoint f
source
instance Finset.decidableDisjoint {α : Type u_1} [DecidableEq α] (U V : Finset α) :
Decidable (Disjoint U V)
Equations

disjoint union #

source
def Finset.disjUnion {α : Type u_1} (s t : Finset α) (h : Disjoint s t) :
Finset α

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.

Equations
Instances For
    source
    @[simp]
    theorem Finset.disjUnion_val {α : Type u_1} (s t : Finset α) (h : Disjoint s t) :
    (s.disjUnion t h).val = s.val + t.val
    source
    @[simp]
    theorem Finset.mem_disjUnion {α : Type u_4} {s t : Finset α} {h : Disjoint s t} {a : α} :
    a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t
    source
    @[simp]
    theorem Finset.coe_disjUnion {α : Type u_1} {s t : Finset α} (h : Disjoint s t) :
    ↑(s.disjUnion t h) = ↑s ∪ ↑t
    source
    theorem Finset.disjUnion_comm {α : Type u_1} (s t : Finset α) (h : Disjoint s t) :
    s.disjUnion t h = t.disjUnion s ⋯
    source
    @[simp]
    theorem Finset.disjUnion_inj_left {α : Type u_1} {s₁ s₂ t : Finset α} (h₁ : Disjoint s₁ t) (h₂ : Disjoint s₂ t) :
    s₁.disjUnion t h₁ = s₂.disjUnion t h₂ ↔ s₁ = s₂
    source
    @[simp]
    theorem Finset.disjUnion_inj_right {α : Type u_1} {s t₁ t₂ : Finset α} (h₁ : Disjoint s t₁) (h₂ : Disjoint s t₂) :
    s.disjUnion t₁ h₁ = s.disjUnion t₂ h₂ ↔ t₁ = t₂
    source
    @[simp]
    theorem Finset.empty_disjUnion {α : Type u_1} (t : Finset α) (h : Disjoint ∅ t := ⋯) :
    ∅.disjUnion t h = t
    source
    @[simp]
    theorem Finset.disjUnion_empty {α : Type u_1} (s : Finset α) (h : Disjoint s ∅ := ⋯) :
    s.disjUnion ∅ h = s
    source
    theorem Finset.singleton_disjUnion {α : Type u_1} (a : α) (t : Finset α) (h : Disjoint {a} t) :
    {a}.disjUnion t h = cons a t ⋯
    source
    theorem Finset.disjUnion_singleton {α : Type u_1} (s : Finset α) (a : α) (h : Disjoint s {a}) :
    s.disjUnion {a} h = cons a s ⋯

    insert #

    source
    @[simp]
    theorem Finset.disjoint_insert_left {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
    Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t
    source
    @[simp]
    theorem Finset.disjoint_insert_right {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
    Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t
    source
    @[simp]
    theorem Multiset.disjoint_toFinset {α : Type u_1} [DecidableEq α] {m1 m2 : Multiset α} :
    Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2
    source
    @[simp]
    theorem List.disjoint_toFinset_iff_disjoint {α : Type u_1} [DecidableEq α] {l l' : List α} :
    _root_.Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l'