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 : ααα
Instances
    class HasInfs (α : Type u_4) :
    Type u_4

    Notation typeclass for pointwise infimum .

    • infs : ααα
    Instances
      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
      Instances For
        @[simp]
        theorem Set.mem_sups {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} {c : α} :
        c s t ∃ a ∈ s, ∃ b ∈ t, a b = c
        theorem Set.sup_mem_sups {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} {a : α} {b : α} :
        a sb ta b s t
        theorem Set.sups_subset {α : Type u_2} [SemilatticeSup α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
        s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
        theorem Set.sups_subset_left {α : Type u_2} [SemilatticeSup α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
        t₁ t₂s t₁ s t₂
        theorem Set.sups_subset_right {α : Type u_2} [SemilatticeSup α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
        s₁ s₂s₁ t s₂ t
        theorem Set.image_subset_sups_left {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} {b : α} :
        b t(fun (a : α) => a b) '' s s t
        theorem Set.image_subset_sups_right {α : Type u_2} [SemilatticeSup α] {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} [SemilatticeSup α] {s : Set α} {t : Set α} {p : αProp} :
        (cs t, p c) as, bt, p (a b)
        @[simp]
        theorem Set.sups_subset_iff {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} {u : Set α} :
        s t u as, bt, a b u
        @[simp]
        theorem Set.sups_nonempty {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} :
        theorem Set.Nonempty.sups {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} :
        theorem Set.Nonempty.of_sups_left {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} :
        theorem Set.Nonempty.of_sups_right {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} :
        @[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 : Set α} {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₁ : Set α} {s₂ : Set α} {t : Set α} :
        (s₁ s₂) t = s₁ t s₂ t
        theorem Set.sups_union_right {α : Type u_2} [SemilatticeSup α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
        s (t₁ t₂) = s t₁ s t₂
        theorem Set.sups_inter_subset_left {α : Type u_2} [SemilatticeSup α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
        (s₁ s₂) t s₁ t s₂ t
        theorem Set.sups_inter_subset_right {α : Type u_2} [SemilatticeSup α] {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} [SemilatticeSup α] [SemilatticeSup β] [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} [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 : 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} [SemilatticeSup α] (s : Set α) (t : Set α) :
        ⋃ a ∈ s, (fun (x x_1 : α) => x x_1) a '' t = s t
        theorem Set.iUnion_image_sup_right {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) :
        ⋃ b ∈ t, (fun (x : α) => x b) '' s = s t
        @[simp]
        theorem Set.image_sup_prod {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) :
        Set.image2 (fun (x x_1 : α) => x x_1) s t = s t
        theorem Set.sups_assoc {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) (u : Set α) :
        s t u = s (t u)
        theorem Set.sups_comm {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) :
        s t = t s
        theorem Set.sups_left_comm {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) (u : Set α) :
        s (t u) = t (s u)
        theorem Set.sups_right_comm {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) (u : Set α) :
        s t u = s u t
        theorem Set.sups_sups_sups_comm {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) (u : Set α) (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
        Instances For
          @[simp]
          theorem Set.mem_infs {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} {c : α} :
          c s t ∃ a ∈ s, ∃ b ∈ t, a b = c
          theorem Set.inf_mem_infs {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} {a : α} {b : α} :
          a sb ta b s t
          theorem Set.infs_subset {α : Type u_2} [SemilatticeInf α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
          s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
          theorem Set.infs_subset_left {α : Type u_2} [SemilatticeInf α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
          t₁ t₂s t₁ s t₂
          theorem Set.infs_subset_right {α : Type u_2} [SemilatticeInf α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
          s₁ s₂s₁ t s₂ t
          theorem Set.image_subset_infs_left {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} {b : α} :
          b t(fun (a : α) => a b) '' s s t
          theorem Set.image_subset_infs_right {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} {a : α} :
          a s(fun (x : α) => a x) '' t s t
          theorem Set.forall_infs_iff {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} {p : αProp} :
          (cs t, p c) as, bt, p (a b)
          @[simp]
          theorem Set.infs_subset_iff {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} {u : Set α} :
          s t u as, bt, a b u
          @[simp]
          theorem Set.infs_nonempty {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} :
          theorem Set.Nonempty.infs {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} :
          theorem Set.Nonempty.of_infs_left {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} :
          theorem Set.Nonempty.of_infs_right {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} :
          @[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 : Set α} {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₁ : Set α} {s₂ : Set α} {t : Set α} :
          (s₁ s₂) t = s₁ t s₂ t
          theorem Set.infs_union_right {α : Type u_2} [SemilatticeInf α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
          s (t₁ t₂) = s t₁ s t₂
          theorem Set.infs_inter_subset_left {α : Type u_2} [SemilatticeInf α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
          (s₁ s₂) t s₁ t s₂ t
          theorem Set.infs_inter_subset_right {α : Type u_2} [SemilatticeInf α] {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} [SemilatticeInf α] [SemilatticeInf β] [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} [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 : 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} [SemilatticeInf α] (s : Set α) (t : Set α) :
          ⋃ a ∈ s, (fun (x : α) => a x) '' t = s t
          theorem Set.iUnion_image_inf_right {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) :
          ⋃ b ∈ t, (fun (x : α) => x b) '' s = s t
          @[simp]
          theorem Set.image_inf_prod {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) :
          Set.image2 (fun (x x_1 : α) => x x_1) s t = s t
          theorem Set.infs_assoc {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) (u : Set α) :
          s t u = s (t u)
          theorem Set.infs_comm {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) :
          s t = t s
          theorem Set.infs_left_comm {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) (u : Set α) :
          s (t u) = t (s u)
          theorem Set.infs_right_comm {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) (u : Set α) :
          s t u = s u t
          theorem Set.infs_infs_infs_comm {α : Type u_2} [SemilatticeInf α] (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} [DistribLattice α] (s : Set α) (t : Set α) (u : Set α) :
          s t u (s t) (s u)
          theorem Set.sups_infs_subset_right {α : Type u_2} [DistribLattice α] (s : Set α) (t : Set α) (u : Set α) :
          t u s (t s) (u s)
          theorem Set.infs_sups_subset_left {α : Type u_2} [DistribLattice α] (s : Set α) (t : Set α) (u : Set α) :
          s (t u) s t s u
          theorem Set.infs_sups_subset_right {α : Type u_2} [DistribLattice α] (s : Set α) (t : Set α) (u : Set α) :
          (t u) s t s u s
          @[simp]
          theorem upperClosure_sups {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) :
          @[simp]
          theorem lowerClosure_infs {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) :