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 scope SetFamily:

• s ⊻ t
• s ⊼ t

References

[B. Bollobás, Combinatorics][bollobas1986]

class HasSups (α : Type u_4) : Type u_4

Notation typeclass for pointwise supremum ⊻.

• sups : α → α → α

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

class HasInfs (α : Type u_4) : Type u_4

Notation typeclass for pointwise infimum ⊼.

• infs : α → α → α

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

def «term_⊻_» : Lean.TrailingParserDescr

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

Equations

• «term_⊻_» = Lean.ParserDescr.trailingNode `«term_⊻_» 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊻ ") (Lean.ParserDescr.cat `term 75))

def «term_⊼_» : Lean.TrailingParserDescr

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

Equations

• «term_⊼_» = Lean.ParserDescr.trailingNode `«term_⊼_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊼ ") (Lean.ParserDescr.cat `term 76))

@[instance_reducible]

def Set.hasSups {α : Type u_2} [SemilatticeSup α] : HasSups (Set α)

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

Equations

• Set.hasSups = { sups := Set.image2 fun (x1 x2 : α) => x1 ⊔ x2 }

@[simp]

theorem Set.mem_sups {α : Type u_2} [SemilatticeSup α] {s t : Set α} {c : α} : c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c

theorem Set.sup_mem_sups {α : Type u_2} [SemilatticeSup α] {s t : Set α} {a b : α} : a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t

theorem Set.sups_subset {α : Type u_2} [SemilatticeSup α] {s₁ s₂ t₁ t₂ : Set α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂

theorem Set.sups_subset_left {α : Type u_2} [SemilatticeSup α] {s t₁ t₂ : Set α} : t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂

theorem Set.sups_subset_right {α : Type u_2} [SemilatticeSup α] {s₁ s₂ t : Set α} : s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t

theorem Set.image_subset_sups_left {α : Type u_2} [SemilatticeSup α] {s t : Set α} {b : α} : b ∈ t → (fun (a : α) => a ⊔ b) '' s ⊆ s ⊻ t

theorem Set.image_subset_sups_right {α : Type u_2} [SemilatticeSup α] {s t : Set α} {a : α} : a ∈ s → (fun (x1 x2 : α) => x1 ⊔ x2) a '' t ⊆ s ⊻ t

theorem Set.forall_sups_iff {α : Type u_2} [SemilatticeSup α] {s t : Set α} {p : α → Prop} : (∀ c ∈ s ⊻ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊔ b)

@[simp]

theorem Set.sups_subset_iff {α : Type u_2} [SemilatticeSup α] {s t u : Set α} : s ⊻ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊔ b ∈ u

@[simp]

theorem Set.sups_nonempty {α : Type u_2} [SemilatticeSup α] {s t : Set α} : (s ⊻ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.sups {α : Type u_2} [SemilatticeSup α] {s t : Set α} : s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty

theorem Set.Nonempty.of_sups_left {α : Type u_2} [SemilatticeSup α] {s t : Set α} : (s ⊻ t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_sups_right {α : Type u_2} [SemilatticeSup α] {s t : Set α} : (s ⊻ t).Nonempty → t.Nonempty

@[simp]

theorem Set.empty_sups {α : Type u_2} [SemilatticeSup α] {t : Set α} : ∅ ⊻ t = ∅

@[simp]

theorem Set.sups_empty {α : Type u_2} [SemilatticeSup α] {s : Set α} : s ⊻ ∅ = ∅

@[simp]

theorem Set.sups_eq_empty {α : Type u_2} [SemilatticeSup α] {s t : Set α} : s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.singleton_sups {α : Type u_2} [SemilatticeSup α] {t : Set α} {a : α} : {a} ⊻ t = (fun (b : α) => a ⊔ b) '' t

@[simp]

theorem Set.sups_singleton {α : Type u_2} [SemilatticeSup α] {s : Set α} {b : α} : s ⊻ {b} = (fun (a : α) => a ⊔ b) '' s

theorem Set.singleton_sups_singleton {α : Type u_2} [SemilatticeSup α] {a b : α} : {a} ⊻ {b} = {a ⊔ b}

theorem Set.sups_union_left {α : Type u_2} [SemilatticeSup α] {s₁ s₂ t : Set α} : (s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t

theorem Set.sups_union_right {α : Type u_2} [SemilatticeSup α] {s t₁ t₂ : Set α} : s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂

theorem Set.sups_inter_subset_left {α : Type u_2} [SemilatticeSup α] {s₁ s₂ t : Set α} : (s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t

theorem Set.sups_inter_subset_right {α : Type u_2} [SemilatticeSup α] {s t₁ t₂ : Set α} : s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂

theorem Set.image_sups {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) (s t : Set α) : ⇑f '' (s ⊻ t) = ⇑f '' s ⊻ ⇑f '' t

theorem Set.subset_sups_self {α : Type u_2} [SemilatticeSup α] {s : Set α} : s ⊆ s ⊻ s

theorem Set.sups_subset_self {α : Type u_2} [SemilatticeSup α] {s : Set α} : s ⊻ s ⊆ s ↔ SupClosed s

@[simp]

theorem Set.sups_eq_self {α : Type u_2} [SemilatticeSup α] {s : Set α} : s ⊻ s = s ↔ SupClosed s

theorem Set.sep_sups_le {α : Type u_2} [SemilatticeSup α] (s 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} [SemilatticeSup α] (s t : Set α) : ⋃ a ∈ s, (fun (x1 x2 : α) => x1 ⊔ x2) a '' t = s ⊻ t

theorem Set.iUnion_image_sup_right {α : Type u_2} [SemilatticeSup α] (s t : Set α) : ⋃ b ∈ t, (fun (x : α) => x ⊔ b) '' s = s ⊻ t

@[simp]

theorem Set.image_sup_prod {α : Type u_2} [SemilatticeSup α] (s t : Set α) : image2 (fun (x1 x2 : α) => x1 ⊔ x2) s t = s ⊻ t

theorem Set.sups_assoc {α : Type u_2} [SemilatticeSup α] (s t u : Set α) : s ⊻ t ⊻ u = s ⊻ (t ⊻ u)

theorem Set.sups_comm {α : Type u_2} [SemilatticeSup α] (s t : Set α) : s ⊻ t = t ⊻ s

theorem Set.sups_left_comm {α : Type u_2} [SemilatticeSup α] (s t u : Set α) : s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)

theorem Set.sups_right_comm {α : Type u_2} [SemilatticeSup α] (s t u : Set α) : s ⊻ t ⊻ u = s ⊻ u ⊻ t

theorem Set.sups_sups_sups_comm {α : Type u_2} [SemilatticeSup α] (s t u v : Set α) : s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)

@[instance_reducible]

def Set.hasInfs {α : Type u_2} [SemilatticeInf α] : HasInfs (Set α)

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

Equations

• Set.hasInfs = { infs := Set.image2 fun (x1 x2 : α) => x1 ⊓ x2 }

@[simp]

theorem Set.mem_infs {α : Type u_2} [SemilatticeInf α] {s t : Set α} {c : α} : c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c

theorem Set.inf_mem_infs {α : Type u_2} [SemilatticeInf α] {s t : Set α} {a b : α} : a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t

theorem Set.infs_subset {α : Type u_2} [SemilatticeInf α] {s₁ s₂ t₁ t₂ : Set α} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂

theorem Set.infs_subset_left {α : Type u_2} [SemilatticeInf α] {s t₁ t₂ : Set α} : t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂

theorem Set.infs_subset_right {α : Type u_2} [SemilatticeInf α] {s₁ s₂ t : Set α} : s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t

theorem Set.image_subset_infs_left {α : Type u_2} [SemilatticeInf α] {s t : Set α} {b : α} : b ∈ t → (fun (a : α) => a ⊓ b) '' s ⊆ s ⊼ t

theorem Set.image_subset_infs_right {α : Type u_2} [SemilatticeInf α] {s t : Set α} {a : α} : a ∈ s → (fun (x : α) => a ⊓ x) '' t ⊆ s ⊼ t

theorem Set.forall_infs_iff {α : Type u_2} [SemilatticeInf α] {s t : Set α} {p : α → Prop} : (∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b)

@[simp]

theorem Set.infs_subset_iff {α : Type u_2} [SemilatticeInf α] {s t u : Set α} : s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u

@[simp]

theorem Set.infs_nonempty {α : Type u_2} [SemilatticeInf α] {s t : Set α} : (s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.infs {α : Type u_2} [SemilatticeInf α] {s t : Set α} : s.Nonempty → t.Nonempty → (s ⊼ t).Nonempty

theorem Set.Nonempty.of_infs_left {α : Type u_2} [SemilatticeInf α] {s t : Set α} : (s ⊼ t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_infs_right {α : Type u_2} [SemilatticeInf α] {s t : Set α} : (s ⊼ t).Nonempty → t.Nonempty

@[simp]

theorem Set.empty_infs {α : Type u_2} [SemilatticeInf α] {t : Set α} : ∅ ⊼ t = ∅

@[simp]

theorem Set.infs_empty {α : Type u_2} [SemilatticeInf α] {s : Set α} : s ⊼ ∅ = ∅

@[simp]

theorem Set.infs_eq_empty {α : Type u_2} [SemilatticeInf α] {s t : Set α} : s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.singleton_infs {α : Type u_2} [SemilatticeInf α] {t : Set α} {a : α} : {a} ⊼ t = (fun (b : α) => a ⊓ b) '' t

@[simp]

theorem Set.infs_singleton {α : Type u_2} [SemilatticeInf α] {s : Set α} {b : α} : s ⊼ {b} = (fun (a : α) => a ⊓ b) '' s

theorem Set.singleton_infs_singleton {α : Type u_2} [SemilatticeInf α] {a b : α} : {a} ⊼ {b} = {a ⊓ b}

theorem Set.infs_union_left {α : Type u_2} [SemilatticeInf α] {s₁ s₂ t : Set α} : (s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t

theorem Set.infs_union_right {α : Type u_2} [SemilatticeInf α] {s t₁ t₂ : Set α} : s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂

theorem Set.infs_inter_subset_left {α : Type u_2} [SemilatticeInf α] {s₁ s₂ t : Set α} : (s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t

theorem Set.infs_inter_subset_right {α : Type u_2} [SemilatticeInf α] {s t₁ t₂ : Set α} : s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂

theorem Set.image_infs {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) (s t : Set α) : ⇑f '' (s ⊼ t) = ⇑f '' s ⊼ ⇑f '' t

theorem Set.subset_infs_self {α : Type u_2} [SemilatticeInf α] {s : Set α} : s ⊆ s ⊼ s

theorem Set.infs_self_subset {α : Type u_2} [SemilatticeInf α] {s : Set α} : s ⊼ s ⊆ s ↔ InfClosed s

@[simp]

theorem Set.infs_self {α : Type u_2} [SemilatticeInf α] {s : Set α} : s ⊼ s = s ↔ InfClosed s

theorem Set.sep_infs_le {α : Type u_2} [SemilatticeInf α] (s 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} [SemilatticeInf α] (s t : Set α) : ⋃ a ∈ s, (fun (x : α) => a ⊓ x) '' t = s ⊼ t

theorem Set.iUnion_image_inf_right {α : Type u_2} [SemilatticeInf α] (s t : Set α) : ⋃ b ∈ t, (fun (x : α) => x ⊓ b) '' s = s ⊼ t

@[simp]

theorem Set.image_inf_prod {α : Type u_2} [SemilatticeInf α] (s t : Set α) : image2 (fun (x x_1 : α) => x ⊓ x_1) s t = s ⊼ t

theorem Set.infs_assoc {α : Type u_2} [SemilatticeInf α] (s t u : Set α) : s ⊼ t ⊼ u = s ⊼ (t ⊼ u)

theorem Set.infs_comm {α : Type u_2} [SemilatticeInf α] (s t : Set α) : s ⊼ t = t ⊼ s

theorem Set.infs_left_comm {α : Type u_2} [SemilatticeInf α] (s t u : Set α) : s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)

theorem Set.infs_right_comm {α : Type u_2} [SemilatticeInf α] (s t u : Set α) : s ⊼ t ⊼ u = s ⊼ u ⊼ t

theorem Set.infs_infs_infs_comm {α : Type u_2} [SemilatticeInf α] (s t u v : Set α) : s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)

@[simp]

theorem Set.infs_eq_inter {α : Type u_2} [SemilatticeInf α] {s t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) : s ⊼ t = s ∩ t

theorem Set.sups_infs_subset_left {α : Type u_2} [DistribLattice α] (s t u : Set α) : s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)

theorem Set.sups_infs_subset_right {α : Type u_2} [DistribLattice α] (s t u : Set α) : t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)

theorem Set.infs_sups_subset_left {α : Type u_2} [DistribLattice α] (s t u : Set α) : s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u

theorem Set.infs_sups_subset_right {α : Type u_2} [DistribLattice α] (s t u : Set α) : (t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s

@[simp]

theorem Set.isLowerSet_powerset {α : Type u_2} (s : Set α) : IsLowerSet (𝒫 s)

@[simp]

theorem upperClosure_sups {α : Type u_2} [SemilatticeSup α] (s t : Set α) : upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t

@[simp]

theorem lowerClosure_infs {α : Type u_2} [SemilatticeInf α] (s t : Set α) : lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t