mathlib3 documentation

data.finset.sups

Set family operations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

Notation #

We define the following notation in locale finset_family:

References #

B. Bollobás, Combinatorics

source
@[protected, instance]
def finset.decidable_pred_mem_upper_closure {α : Type u_1} [preorder α] (s : finset α) [decidable_rel has_le.le] :
decidable_pred (λ (_x : α), _x ∈ upper_closure ↑s)
Equations
source
@[protected, instance]
def finset.decidable_pred_mem_lower_closure {α : Type u_1} [preorder α] (s : finset α) [decidable_rel has_le.le] :
decidable_pred (λ (_x : α), _x ∈ lower_closure ↑s)
Equations
source
@[protected]
def finset.has_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] :
has_sups (finset α)

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

Equations
source
@[simp]
theorem finset.mem_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} {c : α} :
c ∈ s ⊻ t ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ t), a ⊔ b = c
source
@[simp, norm_cast]
theorem finset.coe_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t : finset α) :
↑(s ⊻ t) = ↑s ⊻ ↑t
source
theorem finset.card_sups_le {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t : finset α) :
(s ⊻ t).card ≤ s.card * t.card
source
theorem finset.card_sups_iff {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t : finset α) :
(s ⊻ t).card = s.card * t.card ↔ set.inj_on (λ (x : α × α), x.fst ⊔ x.snd) (↑s ×ˢ ↑t)
source
theorem finset.sup_mem_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} {a b : α} :
a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t
source
theorem finset.sups_subset {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂
source
theorem finset.sups_subset_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t₁ t₂ : finset α} :
t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂
source
theorem finset.sups_subset_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s₁ s₂ t : finset α} :
s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t
source
theorem finset.image_subset_sups_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} {b : α} :
b ∈ t → finset.image (λ (a : α), a ⊔ b) s ⊆ s ⊻ t
source
theorem finset.image_subset_sups_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} {a : α} :
a ∈ s → finset.image (has_sup.sup a) t ⊆ s ⊻ t
source
theorem finset.forall_sups_iff {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s 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} [decidable_eq α] [semilattice_sup α] {s t u : finset α} :
s ⊻ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ⊔ b ∈ u
source
@[simp]
theorem finset.sups_nonempty {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} :
(s ⊻ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[protected]
theorem finset.nonempty.sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} :
s.nonempty → t.nonempty → (s ⊻ t).nonempty
source
theorem finset.nonempty.of_sups_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} :
(s ⊻ t).nonempty → s.nonempty
source
theorem finset.nonempty.of_sups_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} :
(s ⊻ t).nonempty → t.nonempty
source
@[simp]
theorem finset.empty_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] {t : finset α} :
∅ ⊻ t = ∅
source
@[simp]
theorem finset.sups_empty {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s : finset α} :
s ⊻ ∅ = ∅
source
@[simp]
theorem finset.sups_eq_empty {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t : finset α} :
s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.singleton_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] {t : finset α} {a : α} :
{a} ⊻ t = finset.image (λ (b : α), a ⊔ b) t
source
@[simp]
theorem finset.sups_singleton {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s : finset α} {b : α} :
s ⊻ {b} = finset.image (λ (a : α), a ⊔ b) s
source
theorem finset.singleton_sups_singleton {α : Type u_1} [decidable_eq α] [semilattice_sup α] {a b : α} :
{a} ⊻ {b} = {a ⊔ b}
source
theorem finset.sups_union_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s₁ s₂ t : finset α} :
(s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t
source
theorem finset.sups_union_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t₁ t₂ : finset α} :
s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂
source
theorem finset.sups_inter_subset_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s₁ s₂ t : finset α} :
(s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t
source
theorem finset.sups_inter_subset_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] {s t₁ t₂ : finset α} :
s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂
source
theorem finset.subset_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] {u : finset α} {s t : set α} :
↑u ⊆ s ⊻ t → (∃ (s' t' : finset α), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊻ t')
source
theorem finset.bUnion_image_sup_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t : finset α) :
s.bUnion (λ (a : α), finset.image (has_sup.sup a) t) = s ⊻ t
source
theorem finset.bUnion_image_sup_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t : finset α) :
t.bUnion (λ (b : α), finset.image (λ (a : α), a ⊔ b) s) = s ⊻ t
source
@[simp]
theorem finset.image_sup_product {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t : finset α) :
finset.image (function.uncurry has_sup.sup) (s ×ˢ t) = s ⊻ t
source
theorem finset.sups_assoc {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t u : finset α) :
s ⊻ t ⊻ u = s ⊻ (t ⊻ u)
source
theorem finset.sups_comm {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t : finset α) :
s ⊻ t = t ⊻ s
source
theorem finset.sups_left_comm {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t u : finset α) :
s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)
source
theorem finset.sups_right_comm {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t u : finset α) :
s ⊻ t ⊻ u = s ⊻ u ⊻ t
source
theorem finset.sups_sups_sups_comm {α : Type u_1} [decidable_eq α] [semilattice_sup α] (s t u v : finset α) :
s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)
source
theorem finset.filter_sups_le {α : Type u_1} [decidable_eq α] [semilattice_sup α] [decidable_rel has_le.le] (s t : finset α) (a : α) :
finset.filter (λ (b : α), b ≤ a) (s ⊻ t) = finset.filter (λ (b : α), b ≤ a) s ⊻ finset.filter (λ (b : α), b ≤ a) t
source
@[protected]
def finset.has_infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] :
has_infs (finset α)

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

Equations
source
@[simp]
theorem finset.mem_infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} {c : α} :
c ∈ s ⊼ t ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ t), a ⊓ b = c
source
@[simp, norm_cast]
theorem finset.coe_infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t : finset α) :
↑(s ⊼ t) = ↑s ⊼ ↑t
source
theorem finset.card_infs_le {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t : finset α) :
(s ⊼ t).card ≤ s.card * t.card
source
theorem finset.card_infs_iff {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t : finset α) :
(s ⊼ t).card = s.card * t.card ↔ set.inj_on (λ (x : α × α), x.fst ⊓ x.snd) (↑s ×ˢ ↑t)
source
theorem finset.inf_mem_infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} {a b : α} :
a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t
source
theorem finset.infs_subset {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂
source
theorem finset.infs_subset_left {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t₁ t₂ : finset α} :
t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂
source
theorem finset.infs_subset_right {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s₁ s₂ t : finset α} :
s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t
source
theorem finset.image_subset_infs_left {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} {b : α} :
b ∈ t → finset.image (λ (a : α), a ⊓ b) s ⊆ s ⊼ t
source
theorem finset.image_subset_infs_right {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} {a : α} :
a ∈ s → finset.image (has_inf.inf a) t ⊆ s ⊼ t
source
theorem finset.forall_infs_iff {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s 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} [decidable_eq α] [semilattice_inf α] {s t u : finset α} :
s ⊼ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ⊓ b ∈ u
source
@[simp]
theorem finset.infs_nonempty {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} :
(s ⊼ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[protected]
theorem finset.nonempty.infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} :
s.nonempty → t.nonempty → (s ⊼ t).nonempty
source
theorem finset.nonempty.of_infs_left {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} :
(s ⊼ t).nonempty → s.nonempty
source
theorem finset.nonempty.of_infs_right {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} :
(s ⊼ t).nonempty → t.nonempty
source
@[simp]
theorem finset.empty_infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] {t : finset α} :
∅ ⊼ t = ∅
source
@[simp]
theorem finset.infs_empty {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s : finset α} :
s ⊼ ∅ = ∅
source
@[simp]
theorem finset.infs_eq_empty {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t : finset α} :
s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.singleton_infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] {t : finset α} {a : α} :
{a} ⊼ t = finset.image (λ (b : α), a ⊓ b) t
source
@[simp]
theorem finset.infs_singleton {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s : finset α} {b : α} :
s ⊼ {b} = finset.image (λ (a : α), a ⊓ b) s
source
theorem finset.singleton_infs_singleton {α : Type u_1} [decidable_eq α] [semilattice_inf α] {a b : α} :
{a} ⊼ {b} = {a ⊓ b}
source
theorem finset.infs_union_left {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s₁ s₂ t : finset α} :
(s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t
source
theorem finset.infs_union_right {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t₁ t₂ : finset α} :
s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂
source
theorem finset.infs_inter_subset_left {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s₁ s₂ t : finset α} :
(s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t
source
theorem finset.infs_inter_subset_right {α : Type u_1} [decidable_eq α] [semilattice_inf α] {s t₁ t₂ : finset α} :
s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂
source
theorem finset.subset_infs {α : Type u_1} [decidable_eq α] [semilattice_inf α] {u : finset α} {s t : set α} :
↑u ⊆ s ⊼ t → (∃ (s' t' : finset α), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊼ t')
source
theorem finset.bUnion_image_inf_left {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t : finset α) :
s.bUnion (λ (a : α), finset.image (has_inf.inf a) t) = s ⊼ t
source
theorem finset.bUnion_image_inf_right {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t : finset α) :
t.bUnion (λ (b : α), finset.image (λ (a : α), a ⊓ b) s) = s ⊼ t
source
@[simp]
theorem finset.image_inf_product {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t : finset α) :
finset.image (function.uncurry has_inf.inf) (s ×ˢ t) = s ⊼ t
source
theorem finset.infs_assoc {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t u : finset α) :
s ⊼ t ⊼ u = s ⊼ (t ⊼ u)
source
theorem finset.infs_comm {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t : finset α) :
s ⊼ t = t ⊼ s
source
theorem finset.infs_left_comm {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t u : finset α) :
s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)
source
theorem finset.infs_right_comm {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t u : finset α) :
s ⊼ t ⊼ u = s ⊼ u ⊼ t
source
theorem finset.infs_infs_infs_comm {α : Type u_1} [decidable_eq α] [semilattice_inf α] (s t u v : finset α) :
s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)
source
theorem finset.filter_infs_ge {α : Type u_1} [decidable_eq α] [semilattice_inf α] [decidable_rel has_le.le] (s t : finset α) (a : α) :
finset.filter (λ (b : α), a ≤ b) (s ⊼ t) = finset.filter (λ (b : α), a ≤ b) s ⊼ finset.filter (λ (b : α), a ≤ b) t
source
theorem finset.sups_infs_subset_left {α : Type u_1} [decidable_eq α] [distrib_lattice α] (s t u : finset α) :
s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)
source
theorem finset.sups_infs_subset_right {α : Type u_1} [decidable_eq α] [distrib_lattice α] (s t u : finset α) :
t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)
source
theorem finset.infs_sups_subset_left {α : Type u_1} [decidable_eq α] [distrib_lattice α] (s t u : finset α) :
s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u
source
theorem finset.infs_sups_subset_right {α : Type u_1} [decidable_eq α] [distrib_lattice α] (s t u : finset α) :
(t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s
source
def finset.disj_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] (s t : finset α) :
finset α

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

Equations
source
@[simp]
theorem finset.mem_disj_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t : finset α} {c : α} :
c ∈ s.disj_sups t ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ t), disjoint a b ∧ a ⊔ b = c
source
theorem finset.disj_sups_subset_sups {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t : finset α} :
s.disj_sups t ⊆ s ⊻ t
source
theorem finset.card_disj_sups_le {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] (s t : finset α) :
(s.disj_sups t).card ≤ s.card * t.card
source
theorem finset.disj_sups_subset {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁.disj_sups t₁ ⊆ s₂.disj_sups t₂
source
theorem finset.disj_sups_subset_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t₁ t₂ : finset α} (ht : t₁ ⊆ t₂) :
s.disj_sups t₁ ⊆ s.disj_sups t₂
source
theorem finset.disj_sups_subset_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s₁ s₂ t : finset α} (hs : s₁ ⊆ s₂) :
s₁.disj_sups t ⊆ s₂.disj_sups t
source
theorem finset.forall_disj_sups_iff {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t : finset α} {p : α → Prop} :
(∀ (c : α), c ∈ s.disj_sups t → p c) ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → disjoint a b → p (a ⊔ b)
source
@[simp]
theorem finset.disj_sups_subset_iff {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t u : finset α} :
s.disj_sups t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → disjoint a b → a ⊔ b ∈ u
source
theorem finset.nonempty.of_disj_sups_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t : finset α} :
(s.disj_sups t).nonempty → s.nonempty
source
theorem finset.nonempty.of_disj_sups_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t : finset α} :
(s.disj_sups t).nonempty → t.nonempty
source
@[simp]
theorem finset.disj_sups_empty_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {t : finset α} :
∅.disj_sups t = ∅
source
@[simp]
theorem finset.disj_sups_empty_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s : finset α} :
s.disj_sups ∅ = ∅
source
theorem finset.disj_sups_singleton {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {a b : α} :
{a}.disj_sups {b} = ite (disjoint a b) {a ⊔ b} ∅
source
theorem finset.disj_sups_union_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s₁ s₂ t : finset α} :
(s₁ ∪ s₂).disj_sups t = s₁.disj_sups t ∪ s₂.disj_sups t
source
theorem finset.disj_sups_union_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t₁ t₂ : finset α} :
s.disj_sups (t₁ ∪ t₂) = s.disj_sups t₁ ∪ s.disj_sups t₂
source
theorem finset.disj_sups_inter_subset_left {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s₁ s₂ t : finset α} :
(s₁ ∩ s₂).disj_sups t ⊆ s₁.disj_sups t ∩ s₂.disj_sups t
source
theorem finset.disj_sups_inter_subset_right {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] {s t₁ t₂ : finset α} :
s.disj_sups (t₁ ∩ t₂) ⊆ s.disj_sups t₁ ∩ s.disj_sups t₂
source
theorem finset.disj_sups_comm {α : Type u_1} [decidable_eq α] [semilattice_sup α] [order_bot α] [decidable_rel disjoint] (s t : finset α) :
s.disj_sups t = t.disj_sups s
source
theorem finset.disj_sups_assoc {α : Type u_1} [decidable_eq α] [distrib_lattice α] [order_bot α] [decidable_rel disjoint] (s t u : finset α) :
(s.disj_sups t).disj_sups u = s.disj_sups (t.disj_sups u)
source
theorem finset.disj_sups_left_comm {α : Type u_1} [decidable_eq α] [distrib_lattice α] [order_bot α] [decidable_rel disjoint] (s t u : finset α) :
s.disj_sups (t.disj_sups u) = t.disj_sups (s.disj_sups u)
source
theorem finset.disj_sups_right_comm {α : Type u_1} [decidable_eq α] [distrib_lattice α] [order_bot α] [decidable_rel disjoint] (s t u : finset α) :
(s.disj_sups t).disj_sups u = (s.disj_sups u).disj_sups t
source
theorem finset.disj_sups_disj_sups_disj_sups_comm {α : Type u_1} [decidable_eq α] [distrib_lattice α] [order_bot α] [decidable_rel disjoint] (s t u v : finset α) :
(s.disj_sups t).disj_sups (u.disj_sups v) = (s.disj_sups u).disj_sups (t.disj_sups v)