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
      Instances For

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

        Equations
        Instances For
          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 as, bt, 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 (x1 x2 : α) => x1 x2) 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 α} :
            (s t).Nonempty s.Nonempty t.Nonempty
            theorem Set.Nonempty.sups {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} :
            s.Nonemptyt.Nonempty(s t).Nonempty
            theorem Set.Nonempty.of_sups_left {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} :
            (s t).Nonemptys.Nonempty
            theorem Set.Nonempty.of_sups_right {α : Type u_2} [SemilatticeSup α] {s : Set α} {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 : 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 α) :
            as, (fun (x1 x2 : α) => x1 x2) a '' t = s t
            theorem Set.iUnion_image_sup_right {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) :
            bt, (fun (x : α) => x b) '' s = s t
            @[simp]
            theorem Set.image_sup_prod {α : Type u_2} [SemilatticeSup α] (s : Set α) (t : Set α) :
            Set.image2 (fun (x1 x2 : α) => x1 x2) 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 as, bt, 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 α} :
              (s t).Nonempty s.Nonempty t.Nonempty
              theorem Set.Nonempty.infs {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} :
              s.Nonemptyt.Nonempty(s t).Nonempty
              theorem Set.Nonempty.of_infs_left {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} :
              (s t).Nonemptys.Nonempty
              theorem Set.Nonempty.of_infs_right {α : Type u_2} [SemilatticeInf α] {s : Set α} {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 : 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 α) :
              as, (fun (x : α) => a x) '' t = s t
              theorem Set.iUnion_image_inf_right {α : Type u_2} [SemilatticeInf α] (s : Set α) (t : Set α) :
              bt, (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 α) :