Set family operations #

This file defines a few binary operations on Finset α for use in set family combinatorics.

Main declarations #

s ⊻ t: Finset of elements of the form a ⊔ b where a ∈ s, b ∈ t.
s ⊼ t: Finset of elements of the form a ⊓ b where a ∈ s, b ∈ t.
Finset.disjSups s t: Finset of elements of the form a ⊔ b where a ∈ s, b ∈ t and a and b are disjoint.

Notation #

We define the following notation in locale FinsetFamily:

s ⊻ t
s ⊼ t
s ○ t for Finset.disjSups s t

References #

[B. Bollobás, Combinatorics][bollobas1986]

source

def Finset.hasSups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] :

HasSups (Finset α)

s ⊻ t is the finset of elements of the form a ⊔ b where a ∈ s, b ∈ t.

Instances For

source

@[simp]

theorem Finset.mem_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {c : α} :

c ∈ s ⊻ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = c

source

@[simp]

theorem Finset.coe_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

↑(s ⊻ t) = ↑s ⊻ ↑t

source

theorem Finset.card_sups_le {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

Finset.card (s ⊻ t) ≤ Finset.card s * Finset.card t

source

theorem Finset.card_sups_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

Finset.card (s ⊻ t) = Finset.card s * Finset.card t ↔ Set.InjOn (fun x => x.fst ⊔ x.snd) (↑s ×ˢ ↑t)

source

theorem Finset.sup_mem_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} {b : α} :

a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t

source

theorem Finset.sups_subset {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂

source

theorem Finset.sups_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂

source

theorem Finset.sups_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t

source

theorem Finset.image_subset_sups_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {b : α} :

b ∈ t → Finset.image (fun a => a ⊔ b) s ⊆ s ⊻ t

source

theorem Finset.image_subset_sups_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} :

a ∈ s → Finset.image (fun x => a ⊔ x) t ⊆ s ⊻ t

source

theorem Finset.forall_sups_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {p : α → Prop} :

((c : α) → c ∈ s ⊻ t → p c) ↔ (a : α) → a ∈ s → (b : α) → b ∈ t → p (a ⊔ b)

source

@[simp]

theorem Finset.sups_subset_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {u : Finset α} :

s ⊻ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ⊔ b ∈ u

source

@[simp]

theorem Finset.sups_nonempty {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

Finset.Nonempty (s ⊻ t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

source

theorem Finset.Nonempty.sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s ⊻ t)

source

theorem Finset.Nonempty.of_sups_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

Finset.Nonempty (s ⊻ t) → Finset.Nonempty s

source

theorem Finset.Nonempty.of_sups_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

Finset.Nonempty (s ⊻ t) → Finset.Nonempty t

source

@[simp]

theorem Finset.empty_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {t : Finset α} :

∅ ⊻ t = ∅

source

@[simp]

theorem Finset.sups_empty {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :

s ⊻ ∅ = ∅

source

@[simp]

theorem Finset.sups_eq_empty {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem Finset.singleton_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {t : Finset α} {a : α} :

{a} ⊻ t = Finset.image (fun b => a ⊔ b) t

source

@[simp]

theorem Finset.sups_singleton {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {b : α} :

s ⊻ {b} = Finset.image (fun a => a ⊔ b) s

source

theorem Finset.singleton_sups_singleton {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {a : α} {b : α} :

{a} ⊻ {b} = {a ⊔ b}

source

theorem Finset.sups_union_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t

source

theorem Finset.sups_union_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂

source

theorem Finset.sups_inter_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t

source

theorem Finset.sups_inter_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂

source

theorem Finset.subset_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {u : Finset α} {s : Set α} {t : Set α} :

↑u ⊆ s ⊻ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊻ t'

source

theorem Finset.biUnion_image_sup_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

(Finset.biUnion s fun a => Finset.image ((fun x x_1 => x ⊔ x_1) a) t) = s ⊻ t

source

theorem Finset.biUnion_image_sup_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

(Finset.biUnion t fun b => Finset.image (fun a => a ⊔ b) s) = s ⊻ t

source

theorem Finset.image_sup_product {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

Finset.image (Function.uncurry fun x x_1 => x ⊔ x_1) (s ×ˢ t) = s ⊻ t

source

theorem Finset.sups_assoc {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ t ⊻ u = s ⊻ (t ⊻ u)

source

theorem Finset.sups_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

s ⊻ t = t ⊻ s

source

theorem Finset.sups_left_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)

source

theorem Finset.sups_right_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ t ⊻ u = s ⊻ u ⊻ t

source

theorem Finset.sups_sups_sups_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :

s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)

source

def Finset.hasInfs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] :

HasInfs (Finset α)

s ⊼ t is the finset of elements of the form a ⊓ b where a ∈ s, b ∈ t.

Instances For

source

@[simp]

theorem Finset.mem_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {c : α} :

c ∈ s ⊼ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = c

source

@[simp]

theorem Finset.coe_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

↑(s ⊼ t) = ↑s ⊼ ↑t

source

theorem Finset.card_infs_le {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

Finset.card (s ⊼ t) ≤ Finset.card s * Finset.card t

source

theorem Finset.card_infs_iff {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

Finset.card (s ⊼ t) = Finset.card s * Finset.card t ↔ Set.InjOn (fun x => x.fst ⊓ x.snd) (↑s ×ˢ ↑t)

source

theorem Finset.inf_mem_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} {b : α} :

a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t

source

theorem Finset.infs_subset {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂

source

theorem Finset.infs_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂

source

theorem Finset.infs_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t

source

theorem Finset.image_subset_infs_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {b : α} :

b ∈ t → Finset.image (fun a => a ⊓ b) s ⊆ s ⊼ t

source

theorem Finset.image_subset_infs_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} :

a ∈ s → Finset.image (fun x => a ⊓ x) t ⊆ s ⊼ t

source

theorem Finset.forall_infs_iff {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {p : α → Prop} :

((c : α) → c ∈ s ⊼ t → p c) ↔ (a : α) → a ∈ s → (b : α) → b ∈ t → p (a ⊓ b)

source

@[simp]

theorem Finset.infs_subset_iff {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {u : Finset α} :

s ⊼ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ⊓ b ∈ u

source

@[simp]

theorem Finset.infs_nonempty {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

Finset.Nonempty (s ⊼ t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

source

theorem Finset.Nonempty.infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s ⊼ t)

source

theorem Finset.Nonempty.of_infs_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

Finset.Nonempty (s ⊼ t) → Finset.Nonempty s

source

theorem Finset.Nonempty.of_infs_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

Finset.Nonempty (s ⊼ t) → Finset.Nonempty t

source

@[simp]

theorem Finset.empty_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {t : Finset α} :

∅ ⊼ t = ∅

source

@[simp]

theorem Finset.infs_empty {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :

s ⊼ ∅ = ∅

source

@[simp]

theorem Finset.infs_eq_empty {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem Finset.singleton_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {t : Finset α} {a : α} :

{a} ⊼ t = Finset.image (fun b => a ⊓ b) t

source

@[simp]

theorem Finset.infs_singleton {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {b : α} :

s ⊼ {b} = Finset.image (fun a => a ⊓ b) s

source

theorem Finset.singleton_infs_singleton {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {a : α} {b : α} :

{a} ⊼ {b} = {a ⊓ b}

source

theorem Finset.infs_union_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t

source

theorem Finset.infs_union_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂

source

theorem Finset.infs_inter_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t

source

theorem Finset.infs_inter_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂

source

theorem Finset.subset_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {u : Finset α} {s : Set α} {t : Set α} :

↑u ⊆ s ⊼ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊼ t'

source

theorem Finset.biUnion_image_inf_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

(Finset.biUnion s fun a => Finset.image ((fun x x_1 => x ⊓ x_1) a) t) = s ⊼ t

source

theorem Finset.biUnion_image_inf_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

(Finset.biUnion t fun b => Finset.image (fun a => a ⊓ b) s) = s ⊼ t

source

theorem Finset.image_inf_product {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

Finset.image (Function.uncurry fun x x_1 => x ⊓ x_1) (s ×ˢ t) = s ⊼ t

source

theorem Finset.infs_assoc {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ t ⊼ u = s ⊼ (t ⊼ u)

source

theorem Finset.infs_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

s ⊼ t = t ⊼ s

source

theorem Finset.infs_left_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)

source

theorem Finset.infs_right_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ t ⊼ u = s ⊼ u ⊼ t

source

theorem Finset.infs_infs_infs_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :

s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)

source

theorem Finset.sups_infs_subset_left {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)

source

theorem Finset.sups_infs_subset_right {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)

source

theorem Finset.infs_sups_subset_left {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u

source

theorem Finset.infs_sups_subset_right {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

(t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s

source

def Finset.disjSups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :

Finset α

The finset of elements of the form a ⊔ b where a ∈ s, b ∈ t and a and b are disjoint.

Instances For

source

def FinsetFamily.«term_○_» :

Lean.TrailingParserDescr

The finset of elements of the form a ⊔ b where a ∈ s, b ∈ t and a and b are disjoint.

Instances For

source

@[simp]

theorem Finset.mem_disjSups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {c : α} :

c ∈ Finset.disjSups s t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c

source

theorem Finset.disjSups_subset_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :

Finset.disjSups s t ⊆ s ⊻ t

source

theorem Finset.card_disjSups_le {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :

Finset.card (Finset.disjSups s t) ≤ Finset.card s * Finset.card t

source

theorem Finset.disjSups_subset {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :

Finset.disjSups s₁ t₁ ⊆ Finset.disjSups s₂ t₂

source

theorem Finset.disjSups_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (ht : t₁ ⊆ t₂) :

Finset.disjSups s t₁ ⊆ Finset.disjSups s t₂

source

theorem Finset.disjSups_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ ⊆ s₂) :

Finset.disjSups s₁ t ⊆ Finset.disjSups s₂ t

source

theorem Finset.forall_disjSups_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {p : α → Prop} :

((c : α) → c ∈ Finset.disjSups s t → p c) ↔ (a : α) → a ∈ s → (b : α) → b ∈ t → Disjoint a b → p (a ⊔ b)

source

@[simp]

theorem Finset.disjSups_subset_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {u : Finset α} :

Finset.disjSups s t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → a ⊔ b ∈ u

source

theorem Finset.Nonempty.of_disjSups_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :

Finset.Nonempty (Finset.disjSups s t) → Finset.Nonempty s

source

theorem Finset.Nonempty.of_disjSups_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :

Finset.Nonempty (Finset.disjSups s t) → Finset.Nonempty t

source

@[simp]

theorem Finset.disjSups_empty_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {t : Finset α} :

Finset.disjSups ∅ t = ∅

source

@[simp]

theorem Finset.disjSups_empty_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} :

Finset.disjSups s ∅ = ∅

source

theorem Finset.disjSups_singleton {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {a : α} {b : α} :

Finset.disjSups {a} {b} = if Disjoint a b then {a ⊔ b} else ∅

source

theorem Finset.disjSups_union_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

Finset.disjSups (s₁ ∪ s₂) t = Finset.disjSups s₁ t ∪ Finset.disjSups s₂ t

source

theorem Finset.disjSups_union_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

Finset.disjSups s (t₁ ∪ t₂) = Finset.disjSups s t₁ ∪ Finset.disjSups s t₂

source

theorem Finset.disjSups_inter_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

Finset.disjSups (s₁ ∩ s₂) t ⊆ Finset.disjSups s₁ t ∩ Finset.disjSups s₂ t

source

theorem Finset.disjSups_inter_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

Finset.disjSups s (t₁ ∩ t₂) ⊆ Finset.disjSups s t₁ ∩ Finset.disjSups s t₂

source

theorem Finset.disjSups_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :

Finset.disjSups s t = Finset.disjSups t s

source

theorem Finset.disjSups_assoc {α : Type u_1} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) :

Finset.disjSups (Finset.disjSups s t) u = Finset.disjSups s (Finset.disjSups t u)

source

theorem Finset.disjSups_left_comm {α : Type u_1} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) :

Finset.disjSups s (Finset.disjSups t u) = Finset.disjSups t (Finset.disjSups s u)

source

theorem Finset.disjSups_right_comm {α : Type u_1} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) :

Finset.disjSups (Finset.disjSups s t) u = Finset.disjSups (Finset.disjSups s u) t

source

theorem Finset.disjSups_disjSups_disjSups_comm {α : Type u_1} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :

Finset.disjSups (Finset.disjSups s t) (Finset.disjSups u v) = Finset.disjSups (Finset.disjSups s u) (Finset.disjSups t v)