mathlib3 documentation

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 #

Notation #

We define the following notation in locale set_family:

References #

B. Bollobás, Combinatorics

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

Notation typeclass for pointwise supremum ⊻.

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

Notation typeclass for pointwise infimum ⊼.

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

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

Equations
source
@[simp]
theorem set.mem_sups {α : Type u_1} [semilattice_sup α] {s t : set α} {c : α} :
c ∈ s ⊻ t ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ t), a ⊔ b = c
source
theorem set.sup_mem_sups {α : Type u_1} [semilattice_sup α] {s t : set α} {a b : α} :
a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t
source
theorem set.sups_subset {α : Type u_1} [semilattice_sup α] {s₁ s₂ t₁ t₂ : set α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂
source
theorem set.sups_subset_left {α : Type u_1} [semilattice_sup α] {s t₁ t₂ : set α} :
t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂
source
theorem set.sups_subset_right {α : Type u_1} [semilattice_sup α] {s₁ s₂ t : set α} :
s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t
source
theorem set.image_subset_sups_left {α : Type u_1} [semilattice_sup α] {s t : set α} {b : α} :
b ∈ t → (λ (a : α), a ⊔ b) '' s ⊆ s ⊻ t
source
theorem set.image_subset_sups_right {α : Type u_1} [semilattice_sup α] {s t : set α} {a : α} :
a ∈ s → has_sup.sup a '' t ⊆ s ⊻ t
source
theorem set.forall_sups_iff {α : Type u_1} [semilattice_sup α] {s t : set α} {p : α → Prop} :
(∀ (c : α), c ∈ s ⊻ t → p c) ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → p (a ⊔ b)
source
@[simp]
theorem set.sups_subset_iff {α : Type u_1} [semilattice_sup α] {s t u : set α} :
s ⊻ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ⊔ b ∈ u
source
@[simp]
theorem set.sups_nonempty {α : Type u_1} [semilattice_sup α] {s t : set α} :
(s ⊻ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[protected]
theorem set.nonempty.sups {α : Type u_1} [semilattice_sup α] {s t : set α} :
s.nonempty → t.nonempty → (s ⊻ t).nonempty
source
theorem set.nonempty.of_sups_left {α : Type u_1} [semilattice_sup α] {s t : set α} :
(s ⊻ t).nonempty → s.nonempty
source
theorem set.nonempty.of_sups_right {α : Type u_1} [semilattice_sup α] {s t : set α} :
(s ⊻ t).nonempty → t.nonempty
source
@[simp]
theorem set.empty_sups {α : Type u_1} [semilattice_sup α] {t : set α} :
∅ ⊻ t = ∅
source
@[simp]
theorem set.sups_empty {α : Type u_1} [semilattice_sup α] {s : set α} :
s ⊻ ∅ = ∅
source
@[simp]
theorem set.sups_eq_empty {α : Type u_1} [semilattice_sup α] {s t : set α} :
s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem set.singleton_sups {α : Type u_1} [semilattice_sup α] {t : set α} {a : α} :
{a} ⊻ t = (λ (b : α), a ⊔ b) '' t
source
@[simp]
theorem set.sups_singleton {α : Type u_1} [semilattice_sup α] {s : set α} {b : α} :
s ⊻ {b} = (λ (a : α), a ⊔ b) '' s
source
theorem set.singleton_sups_singleton {α : Type u_1} [semilattice_sup α] {a b : α} :
{a} ⊻ {b} = {a ⊔ b}
source
theorem set.sups_union_left {α : Type u_1} [semilattice_sup α] {s₁ s₂ t : set α} :
(s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t
source
theorem set.sups_union_right {α : Type u_1} [semilattice_sup α] {s t₁ t₂ : set α} :
s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂
source
theorem set.sups_inter_subset_left {α : Type u_1} [semilattice_sup α] {s₁ s₂ t : set α} :
(s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t
source
theorem set.sups_inter_subset_right {α : Type u_1} [semilattice_sup α] {s t₁ t₂ : set α} :
s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂
source
theorem set.Union_image_sup_left {α : Type u_1} [semilattice_sup α] (s t : set α) :
(⋃ (a : α) (H : a ∈ s), has_sup.sup a '' t) = s ⊻ t
source
theorem set.Union_image_sup_right {α : Type u_1} [semilattice_sup α] (s t : set α) :
(⋃ (b : α) (H : b ∈ t), (λ (_x : α), _x ⊔ b) '' s) = s ⊻ t
source
@[simp]
theorem set.image_sup_prod {α : Type u_1} [semilattice_sup α] (s t : set α) :
function.uncurry has_sup.sup '' s ×ˢ t = s ⊻ t
source
theorem set.sups_assoc {α : Type u_1} [semilattice_sup α] (s t u : set α) :
s ⊻ t ⊻ u = s ⊻ (t ⊻ u)
source
theorem set.sups_comm {α : Type u_1} [semilattice_sup α] (s t : set α) :
s ⊻ t = t ⊻ s
source
theorem set.sups_left_comm {α : Type u_1} [semilattice_sup α] (s t u : set α) :
s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)
source
theorem set.sups_right_comm {α : Type u_1} [semilattice_sup α] (s t u : set α) :
s ⊻ t ⊻ u = s ⊻ u ⊻ t
source
theorem set.sups_sups_sups_comm {α : Type u_1} [semilattice_sup α] (s t u v : set α) :
s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)
source
@[protected]
def set.has_infs {α : Type u_1} [semilattice_inf α] :
has_infs (set α)

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

Equations
source
@[simp]
theorem set.mem_infs {α : Type u_1} [semilattice_inf α] {s t : set α} {c : α} :
c ∈ s ⊼ t ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ t), a ⊓ b = c
source
theorem set.inf_mem_infs {α : Type u_1} [semilattice_inf α] {s t : set α} {a b : α} :
a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t
source
theorem set.infs_subset {α : Type u_1} [semilattice_inf α] {s₁ s₂ t₁ t₂ : set α} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂
source
theorem set.infs_subset_left {α : Type u_1} [semilattice_inf α] {s t₁ t₂ : set α} :
t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂
source
theorem set.infs_subset_right {α : Type u_1} [semilattice_inf α] {s₁ s₂ t : set α} :
s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t
source
theorem set.image_subset_infs_left {α : Type u_1} [semilattice_inf α] {s t : set α} {b : α} :
b ∈ t → (λ (a : α), a ⊓ b) '' s ⊆ s ⊼ t
source
theorem set.image_subset_infs_right {α : Type u_1} [semilattice_inf α] {s t : set α} {a : α} :
a ∈ s → has_inf.inf a '' t ⊆ s ⊼ t
source
theorem set.forall_infs_iff {α : Type u_1} [semilattice_inf α] {s t : set α} {p : α → Prop} :
(∀ (c : α), c ∈ s ⊼ t → p c) ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → p (a ⊓ b)
source
@[simp]
theorem set.infs_subset_iff {α : Type u_1} [semilattice_inf α] {s t u : set α} :
s ⊼ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ⊓ b ∈ u
source
@[simp]
theorem set.infs_nonempty {α : Type u_1} [semilattice_inf α] {s t : set α} :
(s ⊼ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[protected]
theorem set.nonempty.infs {α : Type u_1} [semilattice_inf α] {s t : set α} :
s.nonempty → t.nonempty → (s ⊼ t).nonempty
source
theorem set.nonempty.of_infs_left {α : Type u_1} [semilattice_inf α] {s t : set α} :
(s ⊼ t).nonempty → s.nonempty
source
theorem set.nonempty.of_infs_right {α : Type u_1} [semilattice_inf α] {s t : set α} :
(s ⊼ t).nonempty → t.nonempty
source
@[simp]
theorem set.empty_infs {α : Type u_1} [semilattice_inf α] {t : set α} :
∅ ⊼ t = ∅
source
@[simp]
theorem set.infs_empty {α : Type u_1} [semilattice_inf α] {s : set α} :
s ⊼ ∅ = ∅
source
@[simp]
theorem set.infs_eq_empty {α : Type u_1} [semilattice_inf α] {s t : set α} :
s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem set.singleton_infs {α : Type u_1} [semilattice_inf α] {t : set α} {a : α} :
{a} ⊼ t = (λ (b : α), a ⊓ b) '' t
source
@[simp]
theorem set.infs_singleton {α : Type u_1} [semilattice_inf α] {s : set α} {b : α} :
s ⊼ {b} = (λ (a : α), a ⊓ b) '' s
source
theorem set.singleton_infs_singleton {α : Type u_1} [semilattice_inf α] {a b : α} :
{a} ⊼ {b} = {a ⊓ b}
source
theorem set.infs_union_left {α : Type u_1} [semilattice_inf α] {s₁ s₂ t : set α} :
(s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t
source
theorem set.infs_union_right {α : Type u_1} [semilattice_inf α] {s t₁ t₂ : set α} :
s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂
source
theorem set.infs_inter_subset_left {α : Type u_1} [semilattice_inf α] {s₁ s₂ t : set α} :
(s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t
source
theorem set.infs_inter_subset_right {α : Type u_1} [semilattice_inf α] {s t₁ t₂ : set α} :
s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂
source
theorem set.Union_image_inf_left {α : Type u_1} [semilattice_inf α] (s t : set α) :
(⋃ (a : α) (H : a ∈ s), has_inf.inf a '' t) = s ⊼ t
source
theorem set.Union_image_inf_right {α : Type u_1} [semilattice_inf α] (s t : set α) :
(⋃ (b : α) (H : b ∈ t), (λ (_x : α), _x ⊓ b) '' s) = s ⊼ t
source
@[simp]
theorem set.image_inf_prod {α : Type u_1} [semilattice_inf α] (s t : set α) :
function.uncurry has_inf.inf '' s ×ˢ t = s ⊼ t
source
theorem set.infs_assoc {α : Type u_1} [semilattice_inf α] (s t u : set α) :
s ⊼ t ⊼ u = s ⊼ (t ⊼ u)
source
theorem set.infs_comm {α : Type u_1} [semilattice_inf α] (s t : set α) :
s ⊼ t = t ⊼ s
source
theorem set.infs_left_comm {α : Type u_1} [semilattice_inf α] (s t u : set α) :
s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)
source
theorem set.infs_right_comm {α : Type u_1} [semilattice_inf α] (s t u : set α) :
s ⊼ t ⊼ u = s ⊼ u ⊼ t
source
theorem set.infs_infs_infs_comm {α : Type u_1} [semilattice_inf α] (s t u v : set α) :
s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)
source
theorem set.sups_infs_subset_left {α : Type u_1} [distrib_lattice α] (s t u : set α) :
s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)
source
theorem set.sups_infs_subset_right {α : Type u_1} [distrib_lattice α] (s t u : set α) :
t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)
source
theorem set.infs_sups_subset_left {α : Type u_1} [distrib_lattice α] (s t u : set α) :
s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u
source
theorem set.infs_sups_subset_right {α : Type u_1} [distrib_lattice α] (s t u : set α) :
(t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s
source
@[simp]
theorem upper_closure_sups {α : Type u_1} [semilattice_sup α] (s t : set α) :
upper_closure (s ⊻ t) = upper_closure s ⊔ upper_closure t
source
@[simp]
theorem lower_closure_infs {α : Type u_1} [semilattice_inf α] (s t : set α) :
lower_closure (s ⊼ t) = lower_closure s ⊓ lower_closure t