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 #

• 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.disj_sups 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 finset_family:

• s ⊻ t
• s ⊼ t
• s ○ t for finset.disj_sups s t

## References #

B. Bollobás, Combinatorics

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

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

Equations
@[simp]
theorem finset.mem_sups {α : Type u_1} [decidable_eq α] {s t : finset α} {c : α} :
c s t (a : α) (H : a s) (b : α) (H : b t), a b = c
@[simp, norm_cast]
theorem finset.coe_sups {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t) = s t
theorem finset.card_sups_le {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).card s.card * t.card
theorem finset.card_sups_iff {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).card = s.card * t.card set.inj_on (λ (x : α × α), x.fst x.snd) (s ×ˢ t)
theorem finset.sup_mem_sups {α : Type u_1} [decidable_eq α] {s t : finset α} {a b : α} :
a s b t a b s t
theorem finset.sups_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ s₂ t₁ t₂ s₁ t₁ s₂ t₂
theorem finset.sups_subset_left {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
t₁ t₂ s t₁ s t₂
theorem finset.sups_subset_right {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} :
s₁ s₂ s₁ t s₂ t
theorem finset.image_subset_sups_left {α : Type u_1} [decidable_eq α] {s t : finset α} {b : α} :
b t finset.image (λ (a : α), a b) s s t
theorem finset.image_subset_sups_right {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a s t s t
theorem finset.forall_sups_iff {α : Type u_1} [decidable_eq α] {s t : finset α} {p : α Prop} :
( (c : α), c s t p c) (a : α), a s (b : α), b t p (a b)
@[simp]
theorem finset.sups_subset_iff {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s t u (a : α), a s (b : α), b t a b u
@[simp]
theorem finset.sups_nonempty {α : Type u_1} [decidable_eq α] {s t : finset α} :
@[protected]
theorem finset.nonempty.sups {α : Type u_1} [decidable_eq α] {s t : finset α} :
theorem finset.nonempty.of_sups_left {α : Type u_1} [decidable_eq α] {s t : finset α} :
theorem finset.nonempty.of_sups_right {α : Type u_1} [decidable_eq α] {s t : finset α} :
@[simp]
theorem finset.empty_sups {α : Type u_1} [decidable_eq α] {t : finset α} :
@[simp]
theorem finset.sups_empty {α : Type u_1} [decidable_eq α] {s : finset α} :
@[simp]
theorem finset.sups_eq_empty {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t = s = t =
@[simp]
theorem finset.singleton_sups {α : Type u_1} [decidable_eq α] {t : finset α} {a : α} :
{a} t = finset.image (λ (b : α), a b) t
@[simp]
theorem finset.sups_singleton {α : Type u_1} [decidable_eq α] {s : finset α} {b : α} :
s {b} = finset.image (λ (a : α), a b) s
theorem finset.singleton_sups_singleton {α : Type u_1} [decidable_eq α] {a b : α} :
{a} {b} = {a b}
theorem finset.sups_union_left {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} :
(s₁ s₂) t = s₁ t s₂ t
theorem finset.sups_union_right {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
s (t₁ t₂) = s t₁ s t₂
theorem finset.sups_inter_subset_left {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} :
(s₁ s₂) t s₁ t s₂ t
theorem finset.sups_inter_subset_right {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
s (t₁ t₂) s t₁ s t₂
theorem finset.subset_sups {α : Type u_1} [decidable_eq α] {u : finset α} {s t : set α} :
u s t ( (s' t' : finset α), s' s t' t u s' t')
theorem finset.bUnion_image_sup_left {α : Type u_1} [decidable_eq α] (s t : finset α) :
s.bUnion (λ (a : α), t) = s t
theorem finset.bUnion_image_sup_right {α : Type u_1} [decidable_eq α] (s t : finset α) :
t.bUnion (λ (b : α), finset.image (λ (a : α), a b) s) = s t
@[simp]
theorem finset.image_sup_product {α : Type u_1} [decidable_eq α] (s t : finset α) :
= s t
theorem finset.sups_assoc {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = s (t u)
theorem finset.sups_comm {α : Type u_1} [decidable_eq α] (s t : finset α) :
s t = t s
theorem finset.sups_left_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) = t (s u)
theorem finset.sups_right_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = s u t
theorem finset.sups_sups_sups_comm {α : Type u_1} [decidable_eq α] (s t u v : finset α) :
s t (u v) = s u (t v)
theorem finset.filter_sups_le {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
finset.filter (λ (b : α), b a) (s t) = finset.filter (λ (b : α), b a) s finset.filter (λ (b : α), b a) t
@[protected]
def finset.has_infs {α : Type u_1} [decidable_eq α]  :

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

Equations
@[simp]
theorem finset.mem_infs {α : Type u_1} [decidable_eq α] {s t : finset α} {c : α} :
c s t (a : α) (H : a s) (b : α) (H : b t), a b = c
@[simp, norm_cast]
theorem finset.coe_infs {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t) = s t
theorem finset.card_infs_le {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).card s.card * t.card
theorem finset.card_infs_iff {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).card = s.card * t.card set.inj_on (λ (x : α × α), x.fst x.snd) (s ×ˢ t)
theorem finset.inf_mem_infs {α : Type u_1} [decidable_eq α] {s t : finset α} {a b : α} :
a s b t a b s t
theorem finset.infs_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ s₂ t₁ t₂ s₁ t₁ s₂ t₂
theorem finset.infs_subset_left {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
t₁ t₂ s t₁ s t₂
theorem finset.infs_subset_right {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} :
s₁ s₂ s₁ t s₂ t
theorem finset.image_subset_infs_left {α : Type u_1} [decidable_eq α] {s t : finset α} {b : α} :
b t finset.image (λ (a : α), a b) s s t
theorem finset.image_subset_infs_right {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a s t s t
theorem finset.forall_infs_iff {α : Type u_1} [decidable_eq α] {s t : finset α} {p : α Prop} :
( (c : α), c s t p c) (a : α), a s (b : α), b t p (a b)
@[simp]
theorem finset.infs_subset_iff {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s t u (a : α), a s (b : α), b t a b u
@[simp]
theorem finset.infs_nonempty {α : Type u_1} [decidable_eq α] {s t : finset α} :
@[protected]
theorem finset.nonempty.infs {α : Type u_1} [decidable_eq α] {s t : finset α} :
theorem finset.nonempty.of_infs_left {α : Type u_1} [decidable_eq α] {s t : finset α} :
theorem finset.nonempty.of_infs_right {α : Type u_1} [decidable_eq α] {s t : finset α} :
@[simp]
theorem finset.empty_infs {α : Type u_1} [decidable_eq α] {t : finset α} :
@[simp]
theorem finset.infs_empty {α : Type u_1} [decidable_eq α] {s : finset α} :
@[simp]
theorem finset.infs_eq_empty {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t = s = t =
@[simp]
theorem finset.singleton_infs {α : Type u_1} [decidable_eq α] {t : finset α} {a : α} :
{a} t = finset.image (λ (b : α), a b) t
@[simp]
theorem finset.infs_singleton {α : Type u_1} [decidable_eq α] {s : finset α} {b : α} :
s {b} = finset.image (λ (a : α), a b) s
theorem finset.singleton_infs_singleton {α : Type u_1} [decidable_eq α] {a b : α} :
{a} {b} = {a b}
theorem finset.infs_union_left {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} :
(s₁ s₂) t = s₁ t s₂ t
theorem finset.infs_union_right {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
s (t₁ t₂) = s t₁ s t₂
theorem finset.infs_inter_subset_left {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} :
(s₁ s₂) t s₁ t s₂ t
theorem finset.infs_inter_subset_right {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
s (t₁ t₂) s t₁ s t₂
theorem finset.subset_infs {α : Type u_1} [decidable_eq α] {u : finset α} {s t : set α} :
u s t ( (s' t' : finset α), s' s t' t u s' t')
theorem finset.bUnion_image_inf_left {α : Type u_1} [decidable_eq α] (s t : finset α) :
s.bUnion (λ (a : α), t) = s t
theorem finset.bUnion_image_inf_right {α : Type u_1} [decidable_eq α] (s t : finset α) :
t.bUnion (λ (b : α), finset.image (λ (a : α), a b) s) = s t
@[simp]
theorem finset.image_inf_product {α : Type u_1} [decidable_eq α] (s t : finset α) :
= s t
theorem finset.infs_assoc {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = s (t u)
theorem finset.infs_comm {α : Type u_1} [decidable_eq α] (s t : finset α) :
s t = t s
theorem finset.infs_left_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) = t (s u)
theorem finset.infs_right_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = s u t
theorem finset.infs_infs_infs_comm {α : Type u_1} [decidable_eq α] (s t u v : finset α) :
s t (u v) = s u (t v)
theorem finset.filter_infs_ge {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
finset.filter (λ (b : α), a b) (s t) = finset.filter (λ (b : α), a b) s finset.filter (λ (b : α), a b) t
theorem finset.sups_infs_subset_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u (s t) (s u)
theorem finset.sups_infs_subset_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
t u s (t s) (u s)
theorem finset.infs_sups_subset_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) s t s u
theorem finset.infs_sups_subset_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
(t u) s t s u s
def finset.disj_sups {α : Type u_1} [decidable_eq α] [order_bot α] (s t : finset α) :

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

Equations
@[simp]
theorem finset.mem_disj_sups {α : Type u_1} [decidable_eq α] [order_bot α] {s t : finset α} {c : α} :
c s.disj_sups t (a : α) (H : a s) (b : α) (H : b t), b a b = c
theorem finset.disj_sups_subset_sups {α : Type u_1} [decidable_eq α] [order_bot α] {s t : finset α} :
s.disj_sups t s t
theorem finset.card_disj_sups_le {α : Type u_1} [decidable_eq α] [order_bot α] (s t : finset α) :
theorem finset.disj_sups_subset {α : Type u_1} [decidable_eq α] [order_bot α] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.disj_sups t₁ s₂.disj_sups t₂
theorem finset.disj_sups_subset_left {α : Type u_1} [decidable_eq α] [order_bot α] {s t₁ t₂ : finset α} (ht : t₁ t₂) :
s.disj_sups t₁ s.disj_sups t₂
theorem finset.disj_sups_subset_right {α : Type u_1} [decidable_eq α] [order_bot α] {s₁ s₂ t : finset α} (hs : s₁ s₂) :
s₁.disj_sups t s₂.disj_sups t
theorem finset.forall_disj_sups_iff {α : Type u_1} [decidable_eq α] [order_bot α] {s t : finset α} {p : α Prop} :
( (c : α), c s.disj_sups t p c) (a : α), a s (b : α), b t b p (a b)
@[simp]
theorem finset.disj_sups_subset_iff {α : Type u_1} [decidable_eq α] [order_bot α] {s t u : finset α} :
s.disj_sups t u (a : α), a s (b : α), b t b a b u
@[simp]
theorem finset.disj_sups_empty_left {α : Type u_1} [decidable_eq α] [order_bot α] {t : finset α} :
@[simp]
theorem finset.disj_sups_empty_right {α : Type u_1} [decidable_eq α] [order_bot α] {s : finset α} :
theorem finset.disj_sups_singleton {α : Type u_1} [decidable_eq α] [order_bot α] {a b : α} :
{a}.disj_sups {b} = ite (disjoint a b) {a b}
theorem finset.disj_sups_union_left {α : Type u_1} [decidable_eq α] [order_bot α] {s₁ s₂ t : finset α} :
(s₁ s₂).disj_sups t = s₁.disj_sups t s₂.disj_sups t
theorem finset.disj_sups_union_right {α : Type u_1} [decidable_eq α] [order_bot α] {s t₁ t₂ : finset α} :
s.disj_sups (t₁ t₂) = s.disj_sups t₁ s.disj_sups t₂
theorem finset.disj_sups_inter_subset_left {α : Type u_1} [decidable_eq α] [order_bot α] {s₁ s₂ t : finset α} :
(s₁ s₂).disj_sups t s₁.disj_sups t s₂.disj_sups t
theorem finset.disj_sups_inter_subset_right {α : Type u_1} [decidable_eq α] [order_bot α] {s t₁ t₂ : finset α} :
s.disj_sups (t₁ t₂) s.disj_sups t₁ s.disj_sups t₂
theorem finset.disj_sups_comm {α : Type u_1} [decidable_eq α] [order_bot α] (s t : finset α) :
theorem finset.disj_sups_assoc {α : Type u_1} [decidable_eq α] [order_bot α] (s t u : finset α) :
theorem finset.disj_sups_left_comm {α : Type u_1} [decidable_eq α] [order_bot α] (s t u : finset α) :
theorem finset.disj_sups_right_comm {α : Type u_1} [decidable_eq α] [order_bot α] (s t u : finset α) :