# Set family operations #

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

## Main declarations #

• s ⊻ t: Set of elements of the form a ⊔ b where a ∈ s, b ∈ t.
• s ⊼ t: Set of elements of the form a ⊓ b where a ∈ s, b ∈ t.

## Notation #

We define the following notation in locale SetFamily:

• s ⊻ t
• s ⊼ t

## References #

B. Bollobás, Combinatorics

class HasSups (α : Type u_4) :
Type u_4

Notation typeclass for pointwise supremum ⊻.

• sups : ααα

The point-wise supremum a ⊔ b of a, b : α.

Instances
class HasInfs (α : Type u_4) :
Type u_4

Notation typeclass for pointwise infimum ⊼.

• infs : ααα

The point-wise infimum a ⊓ b of a, b : α.

Instances

The point-wise supremum a ⊔ b of a, b : α.

Equations
Instances For

The point-wise infimum a ⊓ b of a, b : α.

Equations
Instances For
def Set.hasSups {α : Type u_2} [] :

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

Equations
Instances For
@[simp]
theorem Set.mem_sups {α : Type u_2} [] {s : Set α} {t : Set α} {c : α} :
c s t as, bt, a b = c
theorem Set.sup_mem_sups {α : Type u_2} [] {s : Set α} {t : Set α} {a : α} {b : α} :
a sb ta b s t
theorem Set.sups_subset {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
theorem Set.sups_subset_left {α : Type u_2} [] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
t₁ t₂s t₁ s t₂
theorem Set.sups_subset_right {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂s₁ t s₂ t
theorem Set.image_subset_sups_left {α : Type u_2} [] {s : Set α} {t : Set α} {b : α} :
b t(fun (a : α) => a b) '' s s t
theorem Set.image_subset_sups_right {α : Type u_2} [] {s : Set α} {t : Set α} {a : α} :
a s(fun (x x_1 : α) => x x_1) a '' t s t
theorem Set.forall_sups_iff {α : Type u_2} [] {s : Set α} {t : Set α} {p : αProp} :
(cs t, p c) as, bt, p (a b)
@[simp]
theorem Set.sups_subset_iff {α : Type u_2} [] {s : Set α} {t : Set α} {u : Set α} :
s t u as, bt, a b u
@[simp]
theorem Set.sups_nonempty {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).Nonempty s.Nonempty t.Nonempty
theorem Set.Nonempty.sups {α : Type u_2} [] {s : Set α} {t : Set α} :
s.Nonemptyt.Nonempty(s t).Nonempty
theorem Set.Nonempty.of_sups_left {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).Nonemptys.Nonempty
theorem Set.Nonempty.of_sups_right {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).Nonemptyt.Nonempty
@[simp]
theorem Set.empty_sups {α : Type u_2} [] {t : Set α} :
@[simp]
theorem Set.sups_empty {α : Type u_2} [] {s : Set α} :
@[simp]
theorem Set.sups_eq_empty {α : Type u_2} [] {s : Set α} {t : Set α} :
s t = s = t =
@[simp]
theorem Set.singleton_sups {α : Type u_2} [] {t : Set α} {a : α} :
{a} t = (fun (b : α) => a b) '' t
@[simp]
theorem Set.sups_singleton {α : Type u_2} [] {s : Set α} {b : α} :
s {b} = (fun (a : α) => a b) '' s
theorem Set.singleton_sups_singleton {α : Type u_2} [] {a : α} {b : α} :
{a} {b} = {a b}
theorem Set.sups_union_left {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
(s₁ s₂) t = s₁ t s₂ t
theorem Set.sups_union_right {α : Type u_2} [] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s (t₁ t₂) = s t₁ s t₂
theorem Set.sups_inter_subset_left {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
(s₁ s₂) t s₁ t s₂ t
theorem Set.sups_inter_subset_right {α : Type u_2} [] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s (t₁ t₂) s t₁ s t₂
theorem Set.image_sups {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [SupHomClass F α β] (f : F) (s : Set α) (t : Set α) :
f '' (s t) = f '' s f '' t
theorem Set.subset_sups_self {α : Type u_2} [] {s : Set α} :
s s s
theorem Set.sups_subset_self {α : Type u_2} [] {s : Set α} :
s s s
@[simp]
theorem Set.sups_eq_self {α : Type u_2} [] {s : Set α} :
s s = s
theorem Set.sep_sups_le {α : Type u_2} [] (s : Set α) (t : Set α) (a : α) :
{b : α | b s t b a} = {b : α | b s b a} {b : α | b t b a}
theorem Set.iUnion_image_sup_left {α : Type u_2} [] (s : Set α) (t : Set α) :
as, (fun (x x_1 : α) => x x_1) a '' t = s t
theorem Set.iUnion_image_sup_right {α : Type u_2} [] (s : Set α) (t : Set α) :
bt, (fun (x : α) => x b) '' s = s t
@[simp]
theorem Set.image_sup_prod {α : Type u_2} [] (s : Set α) (t : Set α) :
Set.image2 (fun (x x_1 : α) => x x_1) s t = s t
theorem Set.sups_assoc {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s t u = s (t u)
theorem Set.sups_comm {α : Type u_2} [] (s : Set α) (t : Set α) :
s t = t s
theorem Set.sups_left_comm {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s (t u) = t (s u)
theorem Set.sups_right_comm {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s t u = s u t
theorem Set.sups_sups_sups_comm {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) (v : Set α) :
s t (u v) = s u (t v)
def Set.hasInfs {α : Type u_2} [] :

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

Equations
Instances For
@[simp]
theorem Set.mem_infs {α : Type u_2} [] {s : Set α} {t : Set α} {c : α} :
c s t as, bt, a b = c
theorem Set.inf_mem_infs {α : Type u_2} [] {s : Set α} {t : Set α} {a : α} {b : α} :
a sb ta b s t
theorem Set.infs_subset {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
theorem Set.infs_subset_left {α : Type u_2} [] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
t₁ t₂s t₁ s t₂
theorem Set.infs_subset_right {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂s₁ t s₂ t
theorem Set.image_subset_infs_left {α : Type u_2} [] {s : Set α} {t : Set α} {b : α} :
b t(fun (a : α) => a b) '' s s t
theorem Set.image_subset_infs_right {α : Type u_2} [] {s : Set α} {t : Set α} {a : α} :
a s(fun (x : α) => a x) '' t s t
theorem Set.forall_infs_iff {α : Type u_2} [] {s : Set α} {t : Set α} {p : αProp} :
(cs t, p c) as, bt, p (a b)
@[simp]
theorem Set.infs_subset_iff {α : Type u_2} [] {s : Set α} {t : Set α} {u : Set α} :
s t u as, bt, a b u
@[simp]
theorem Set.infs_nonempty {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).Nonempty s.Nonempty t.Nonempty
theorem Set.Nonempty.infs {α : Type u_2} [] {s : Set α} {t : Set α} :
s.Nonemptyt.Nonempty(s t).Nonempty
theorem Set.Nonempty.of_infs_left {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).Nonemptys.Nonempty
theorem Set.Nonempty.of_infs_right {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).Nonemptyt.Nonempty
@[simp]
theorem Set.empty_infs {α : Type u_2} [] {t : Set α} :
@[simp]
theorem Set.infs_empty {α : Type u_2} [] {s : Set α} :
@[simp]
theorem Set.infs_eq_empty {α : Type u_2} [] {s : Set α} {t : Set α} :
s t = s = t =
@[simp]
theorem Set.singleton_infs {α : Type u_2} [] {t : Set α} {a : α} :
{a} t = (fun (b : α) => a b) '' t
@[simp]
theorem Set.infs_singleton {α : Type u_2} [] {s : Set α} {b : α} :
s {b} = (fun (a : α) => a b) '' s
theorem Set.singleton_infs_singleton {α : Type u_2} [] {a : α} {b : α} :
{a} {b} = {a b}
theorem Set.infs_union_left {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
(s₁ s₂) t = s₁ t s₂ t
theorem Set.infs_union_right {α : Type u_2} [] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s (t₁ t₂) = s t₁ s t₂
theorem Set.infs_inter_subset_left {α : Type u_2} [] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
(s₁ s₂) t s₁ t s₂ t
theorem Set.infs_inter_subset_right {α : Type u_2} [] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s (t₁ t₂) s t₁ s t₂
theorem Set.image_infs {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [InfHomClass F α β] (f : F) (s : Set α) (t : Set α) :
f '' (s t) = f '' s f '' t
theorem Set.subset_infs_self {α : Type u_2} [] {s : Set α} :
s s s
theorem Set.infs_self_subset {α : Type u_2} [] {s : Set α} :
s s s
@[simp]
theorem Set.infs_self {α : Type u_2} [] {s : Set α} :
s s = s
theorem Set.sep_infs_le {α : Type u_2} [] (s : Set α) (t : Set α) (a : α) :
{b : α | b s t a b} = {b : α | b s a b} {b : α | b t a b}
theorem Set.iUnion_image_inf_left {α : Type u_2} [] (s : Set α) (t : Set α) :
as, (fun (x : α) => a x) '' t = s t
theorem Set.iUnion_image_inf_right {α : Type u_2} [] (s : Set α) (t : Set α) :
bt, (fun (x : α) => x b) '' s = s t
@[simp]
theorem Set.image_inf_prod {α : Type u_2} [] (s : Set α) (t : Set α) :
Set.image2 (fun (x x_1 : α) => x x_1) s t = s t
theorem Set.infs_assoc {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s t u = s (t u)
theorem Set.infs_comm {α : Type u_2} [] (s : Set α) (t : Set α) :
s t = t s
theorem Set.infs_left_comm {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s (t u) = t (s u)
theorem Set.infs_right_comm {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s t u = s u t
theorem Set.infs_infs_infs_comm {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) (v : Set α) :
s t (u v) = s u (t v)
theorem Set.sups_infs_subset_left {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s t u (s t) (s u)
theorem Set.sups_infs_subset_right {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
t u s (t s) (u s)
theorem Set.infs_sups_subset_left {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
s (t u) s t s u
theorem Set.infs_sups_subset_right {α : Type u_2} [] (s : Set α) (t : Set α) (u : Set α) :
(t u) s t s u s
@[simp]
theorem upperClosure_sups {α : Type u_2} [] (s : Set α) (t : Set α) :
@[simp]
theorem lowerClosure_infs {α : Type u_2} [] (s : Set α) (t : Set α) :