data.set.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 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 set_family:

• s ⊻ t
• s ⊼ t

## References #

B. Bollobás, Combinatorics

@[class]
structure has_sups (α : Type u_2) :
Type u_2

Notation typeclass for pointwise supremum ⊻.

Instances for has_sups
• has_sups.has_sizeof_inst
@[class]
structure has_infs (α : Type u_2) :
Type u_2

Notation typeclass for pointwise infimum ⊼.

Instances for has_infs
• has_infs.has_sizeof_inst
@[protected]
def set.has_sups {α : Type u_1}  :

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

Equations
@[simp]
theorem set.mem_sups {α : Type u_1} {s t : set α} {c : α} :
c s t (a : α) (H : a s) (b : α) (H : b t), a b = c
theorem set.sup_mem_sups {α : Type u_1} {s t : set α} {a b : α} :
a s b t a b s t
theorem set.sups_subset {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} :
s₁ s₂ t₁ t₂ s₁ t₁ s₂ t₂
theorem set.sups_subset_left {α : Type u_1} {s t₁ t₂ : set α} :
t₁ t₂ s t₁ s t₂
theorem set.sups_subset_right {α : Type u_1} {s₁ s₂ t : set α} :
s₁ s₂ s₁ t s₂ t
theorem set.image_subset_sups_left {α : Type u_1} {s t : set α} {b : α} :
b t (λ (a : α), a b) '' s s t
theorem set.image_subset_sups_right {α : Type u_1} {s t : set α} {a : α} :
a s s t
theorem set.forall_sups_iff {α : Type u_1} {s t : set α} {p : α Prop} :
( (c : α), c s t p c) (a : α), a s (b : α), b t p (a b)
@[simp]
theorem set.sups_subset_iff {α : Type u_1} {s t u : set α} :
s t u (a : α), a s (b : α), b t a b u
@[simp]
theorem set.sups_nonempty {α : Type u_1} {s t : set α} :
@[protected]
theorem set.nonempty.sups {α : Type u_1} {s t : set α} :
theorem set.nonempty.of_sups_left {α : Type u_1} {s t : set α} :
theorem set.nonempty.of_sups_right {α : Type u_1} {s t : set α} :
@[simp]
theorem set.empty_sups {α : Type u_1} {t : set α} :
@[simp]
theorem set.sups_empty {α : Type u_1} {s : set α} :
@[simp]
theorem set.sups_eq_empty {α : Type u_1} {s t : set α} :
s t = s = t =
@[simp]
theorem set.singleton_sups {α : Type u_1} {t : set α} {a : α} :
{a} t = (λ (b : α), a b) '' t
@[simp]
theorem set.sups_singleton {α : Type u_1} {s : set α} {b : α} :
s {b} = (λ (a : α), a b) '' s
theorem set.singleton_sups_singleton {α : Type u_1} {a b : α} :
{a} {b} = {a b}
theorem set.sups_union_left {α : Type u_1} {s₁ s₂ t : set α} :
(s₁ s₂) t = s₁ t s₂ t
theorem set.sups_union_right {α : Type u_1} {s t₁ t₂ : set α} :
s (t₁ t₂) = s t₁ s t₂
theorem set.sups_inter_subset_left {α : Type u_1} {s₁ s₂ t : set α} :
(s₁ s₂) t s₁ t s₂ t
theorem set.sups_inter_subset_right {α : Type u_1} {s t₁ t₂ : set α} :
s (t₁ t₂) s t₁ s t₂
theorem set.Union_image_sup_left {α : Type u_1} (s t : set α) :
( (a : α) (H : a s), '' t) = s t
theorem set.Union_image_sup_right {α : Type u_1} (s t : set α) :
( (b : α) (H : b t), (λ (_x : α), _x b) '' s) = s t
@[simp]
theorem set.image_sup_prod {α : Type u_1} (s t : set α) :
= s t
theorem set.sups_assoc {α : Type u_1} (s t u : set α) :
s t u = s (t u)
theorem set.sups_comm {α : Type u_1} (s t : set α) :
s t = t s
theorem set.sups_left_comm {α : Type u_1} (s t u : set α) :
s (t u) = t (s u)
theorem set.sups_right_comm {α : Type u_1} (s t u : set α) :
s t u = s u t
theorem set.sups_sups_sups_comm {α : Type u_1} (s t u v : set α) :
s t (u v) = s u (t v)
@[protected]
def set.has_infs {α : Type u_1}  :

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

Equations
@[simp]
theorem set.mem_infs {α : Type u_1} {s t : set α} {c : α} :
c s t (a : α) (H : a s) (b : α) (H : b t), a b = c
theorem set.inf_mem_infs {α : Type u_1} {s t : set α} {a b : α} :
a s b t a b s t
theorem set.infs_subset {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} :
s₁ s₂ t₁ t₂ s₁ t₁ s₂ t₂
theorem set.infs_subset_left {α : Type u_1} {s t₁ t₂ : set α} :
t₁ t₂ s t₁ s t₂
theorem set.infs_subset_right {α : Type u_1} {s₁ s₂ t : set α} :
s₁ s₂ s₁ t s₂ t
theorem set.image_subset_infs_left {α : Type u_1} {s t : set α} {b : α} :
b t (λ (a : α), a b) '' s s t
theorem set.image_subset_infs_right {α : Type u_1} {s t : set α} {a : α} :
a s s t
theorem set.forall_infs_iff {α : Type u_1} {s t : set α} {p : α Prop} :
( (c : α), c s t p c) (a : α), a s (b : α), b t p (a b)
@[simp]
theorem set.infs_subset_iff {α : Type u_1} {s t u : set α} :
s t u (a : α), a s (b : α), b t a b u
@[simp]
theorem set.infs_nonempty {α : Type u_1} {s t : set α} :
@[protected]
theorem set.nonempty.infs {α : Type u_1} {s t : set α} :
theorem set.nonempty.of_infs_left {α : Type u_1} {s t : set α} :
theorem set.nonempty.of_infs_right {α : Type u_1} {s t : set α} :
@[simp]
theorem set.empty_infs {α : Type u_1} {t : set α} :
@[simp]
theorem set.infs_empty {α : Type u_1} {s : set α} :
@[simp]
theorem set.infs_eq_empty {α : Type u_1} {s t : set α} :
s t = s = t =
@[simp]
theorem set.singleton_infs {α : Type u_1} {t : set α} {a : α} :
{a} t = (λ (b : α), a b) '' t
@[simp]
theorem set.infs_singleton {α : Type u_1} {s : set α} {b : α} :
s {b} = (λ (a : α), a b) '' s
theorem set.singleton_infs_singleton {α : Type u_1} {a b : α} :
{a} {b} = {a b}
theorem set.infs_union_left {α : Type u_1} {s₁ s₂ t : set α} :
(s₁ s₂) t = s₁ t s₂ t
theorem set.infs_union_right {α : Type u_1} {s t₁ t₂ : set α} :
s (t₁ t₂) = s t₁ s t₂
theorem set.infs_inter_subset_left {α : Type u_1} {s₁ s₂ t : set α} :
(s₁ s₂) t s₁ t s₂ t
theorem set.infs_inter_subset_right {α : Type u_1} {s t₁ t₂ : set α} :
s (t₁ t₂) s t₁ s t₂
theorem set.Union_image_inf_left {α : Type u_1} (s t : set α) :
( (a : α) (H : a s), '' t) = s t
theorem set.Union_image_inf_right {α : Type u_1} (s t : set α) :
( (b : α) (H : b t), (λ (_x : α), _x b) '' s) = s t
@[simp]
theorem set.image_inf_prod {α : Type u_1} (s t : set α) :
= s t
theorem set.infs_assoc {α : Type u_1} (s t u : set α) :
s t u = s (t u)
theorem set.infs_comm {α : Type u_1} (s t : set α) :
s t = t s
theorem set.infs_left_comm {α : Type u_1} (s t u : set α) :
s (t u) = t (s u)
theorem set.infs_right_comm {α : Type u_1} (s t u : set α) :
s t u = s u t
theorem set.infs_infs_infs_comm {α : Type u_1} (s t u v : set α) :
s t (u v) = s u (t v)
theorem set.sups_infs_subset_left {α : Type u_1} (s t u : set α) :
s t u (s t) (s u)
theorem set.sups_infs_subset_right {α : Type u_1} (s t u : set α) :
t u s (t s) (u s)
theorem set.infs_sups_subset_left {α : Type u_1} (s t u : set α) :
s (t u) s t s u
theorem set.infs_sups_subset_right {α : Type u_1} (s t u : set α) :
(t u) s t s u s
@[simp]
theorem upper_closure_sups {α : Type u_1} (s t : set α) :
@[simp]
theorem lower_closure_infs {α : Type u_1} (s t : set α) :