Documentation

Mathlib.Data.Set.Sups

Set family operations #

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

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 : α.

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

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

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

      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_2} [SemilatticeSup α] {s t : Set α} {c : α} :
      c s t as, bt, ab = c
      theorem Set.sup_mem_sups {α : Type u_2} [SemilatticeSup α] {s t : Set α} {a b : α} :
      a sb tab 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 : α) => ab) '' s s t
      theorem Set.image_subset_sups_right {α : Type u_2} [SemilatticeSup α] {s t : Set α} {a : α} :
      a s(fun (x1 x2 : α) => x1x2) a '' t s t
      theorem Set.forall_sups_iff {α : Type u_2} [SemilatticeSup α] {s t : Set α} {p : αProp} :
      (∀ cs t, p c) as, bt, p (ab)
      @[simp]
      theorem Set.sups_subset_iff {α : Type u_2} [SemilatticeSup α] {s t u : Set α} :
      s t u as, bt, ab u
      @[simp]
      theorem Set.sups_nonempty {α : Type u_2} [SemilatticeSup α] {s t : Set α} :
      theorem Set.Nonempty.sups {α : Type u_2} [SemilatticeSup α] {s t : Set α} :
      s.Nonemptyt.Nonempty(s t).Nonempty
      theorem Set.Nonempty.of_sups_left {α : Type u_2} [SemilatticeSup α] {s t : Set α} :
      (s t).Nonemptys.Nonempty
      theorem Set.Nonempty.of_sups_right {α : Type u_2} [SemilatticeSup α] {s t : Set α} :
      (s t).Nonemptyt.Nonempty
      @[simp]
      theorem Set.empty_sups {α : Type u_2} [SemilatticeSup α] {t : Set α} :
      @[simp]
      theorem Set.sups_empty {α : Type u_2} [SemilatticeSup α] {s : Set α} :
      @[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 : α) => ab) '' t
      @[simp]
      theorem Set.sups_singleton {α : Type u_2} [SemilatticeSup α] {s : Set α} {b : α} :
      s {b} = (fun (a : α) => ab) '' s
      theorem Set.singleton_sups_singleton {α : Type u_2} [SemilatticeSup α] {a b : α} :
      {a} {b} = {ab}
      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 α} :
      @[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 α) :
      as, (fun (x1 x2 : α) => x1x2) a '' t = s t
      theorem Set.iUnion_image_sup_right {α : Type u_2} [SemilatticeSup α] (s t : Set α) :
      bt, (fun (x : α) => xb) '' s = s t
      @[simp]
      theorem Set.image_sup_prod {α : Type u_2} [SemilatticeSup α] (s t : Set α) :
      image2 (fun (x1 x2 : α) => x1x2) 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)
      def Set.hasInfs {α : Type u_2} [SemilatticeInf α] :

      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_2} [SemilatticeInf α] {s t : Set α} {c : α} :
      c s t as, bt, ab = c
      theorem Set.inf_mem_infs {α : Type u_2} [SemilatticeInf α] {s t : Set α} {a b : α} :
      a sb tab 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 : α) => ab) '' s s t
      theorem Set.image_subset_infs_right {α : Type u_2} [SemilatticeInf α] {s t : Set α} {a : α} :
      a s(fun (x : α) => ax) '' t s t
      theorem Set.forall_infs_iff {α : Type u_2} [SemilatticeInf α] {s t : Set α} {p : αProp} :
      (∀ cs t, p c) as, bt, p (ab)
      @[simp]
      theorem Set.infs_subset_iff {α : Type u_2} [SemilatticeInf α] {s t u : Set α} :
      s t u as, bt, ab u
      @[simp]
      theorem Set.infs_nonempty {α : Type u_2} [SemilatticeInf α] {s t : Set α} :
      theorem Set.Nonempty.infs {α : Type u_2} [SemilatticeInf α] {s t : Set α} :
      s.Nonemptyt.Nonempty(s t).Nonempty
      theorem Set.Nonempty.of_infs_left {α : Type u_2} [SemilatticeInf α] {s t : Set α} :
      (s t).Nonemptys.Nonempty
      theorem Set.Nonempty.of_infs_right {α : Type u_2} [SemilatticeInf α] {s t : Set α} :
      (s t).Nonemptyt.Nonempty
      @[simp]
      theorem Set.empty_infs {α : Type u_2} [SemilatticeInf α] {t : Set α} :
      @[simp]
      theorem Set.infs_empty {α : Type u_2} [SemilatticeInf α] {s : Set α} :
      @[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 : α) => ab) '' t
      @[simp]
      theorem Set.infs_singleton {α : Type u_2} [SemilatticeInf α] {s : Set α} {b : α} :
      s {b} = (fun (a : α) => ab) '' s
      theorem Set.singleton_infs_singleton {α : Type u_2} [SemilatticeInf α] {a b : α} :
      {a} {b} = {ab}
      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 α} :
      @[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 α) :
      as, (fun (x : α) => ax) '' t = s t
      theorem Set.iUnion_image_inf_right {α : Type u_2} [SemilatticeInf α] (s t : Set α) :
      bt, (fun (x : α) => xb) '' s = s t
      @[simp]
      theorem Set.image_inf_prod {α : Type u_2} [SemilatticeInf α] (s t : Set α) :
      image2 (fun (x x_1 : α) => xx_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)
      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 upperClosure_sups {α : Type u_2} [SemilatticeSup α] (s t : Set α) :
      @[simp]
      theorem lowerClosure_infs {α : Type u_2} [SemilatticeInf α] (s t : Set α) :