Documentation

Mathlib.Data.Finset.Sups

Set family operations #

This file defines a few binary operations on Finset α for use in set family combinatorics.

Main declarations #

Notation #

We define the following notation in locale FinsetFamily:

References #

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

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

Instances For
    @[simp]
    theorem Finset.mem_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {c : α} :
    c s t a, a s b, b t a b = c
    @[simp]
    theorem Finset.coe_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    ↑(s t) = s t
    theorem Finset.card_sups_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    Finset.card (s t) = Finset.card s * Finset.card t Set.InjOn (fun x => x.fst x.snd) (s ×ˢ t)
    theorem Finset.sup_mem_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
    a sb ta b s t
    theorem Finset.sups_subset {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
    s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
    theorem Finset.sups_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
    t₁ t₂s t₁ s t₂
    theorem Finset.sups_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
    s₁ s₂s₁ t s₂ t
    theorem Finset.image_subset_sups_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {b : α} :
    b tFinset.image (fun a => a b) s s t
    theorem Finset.image_subset_sups_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} :
    a sFinset.image (fun x => a x) t s t
    theorem Finset.forall_sups_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {p : αProp} :
    ((c : α) → c s tp c) (a : α) → a s(b : α) → b tp (a b)
    @[simp]
    theorem Finset.sups_subset_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {u : Finset α} :
    s t u ∀ (a : α), a s∀ (b : α), b ta b u
    @[simp]
    theorem Finset.empty_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {t : Finset α} :
    @[simp]
    theorem Finset.sups_empty {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :
    @[simp]
    theorem Finset.sups_eq_empty {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :
    s t = s = t =
    @[simp]
    theorem Finset.singleton_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {t : Finset α} {a : α} :
    {a} t = Finset.image (fun b => a b) t
    @[simp]
    theorem Finset.sups_singleton {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {b : α} :
    s {b} = Finset.image (fun a => a b) s
    theorem Finset.singleton_sups_singleton {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {a : α} {b : α} :
    {a} {b} = {a b}
    theorem Finset.sups_union_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
    (s₁ s₂) t = s₁ t s₂ t
    theorem Finset.sups_union_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
    s (t₁ t₂) = s t₁ s t₂
    theorem Finset.sups_inter_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
    (s₁ s₂) t s₁ t s₂ t
    theorem Finset.sups_inter_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
    s (t₁ t₂) s t₁ s t₂
    theorem Finset.subset_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] {u : Finset α} {s : Set α} {t : Set α} :
    u s ts' t', s' s t' t u s' t'
    theorem Finset.biUnion_image_sup_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    (Finset.biUnion s fun a => Finset.image ((fun x x_1 => x x_1) a) t) = s t
    theorem Finset.biUnion_image_sup_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    (Finset.biUnion t fun b => Finset.image (fun a => a b) s) = s t
    theorem Finset.image_sup_product {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    Finset.image (Function.uncurry fun x x_1 => x x_1) (s ×ˢ t) = s t
    theorem Finset.sups_assoc {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :
    s t u = s (t u)
    theorem Finset.sups_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    s t = t s
    theorem Finset.sups_left_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :
    s (t u) = t (s u)
    theorem Finset.sups_right_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :
    s t u = s u t
    theorem Finset.sups_sups_sups_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :
    s t (u v) = s u (t v)

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

    Instances For
      @[simp]
      theorem Finset.mem_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {c : α} :
      c s t a, a s b, b t a b = c
      @[simp]
      theorem Finset.coe_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      ↑(s t) = s t
      theorem Finset.card_infs_iff {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      Finset.card (s t) = Finset.card s * Finset.card t Set.InjOn (fun x => x.fst x.snd) (s ×ˢ t)
      theorem Finset.inf_mem_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
      a sb ta b s t
      theorem Finset.infs_subset {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
      s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
      theorem Finset.infs_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
      t₁ t₂s t₁ s t₂
      theorem Finset.infs_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
      s₁ s₂s₁ t s₂ t
      theorem Finset.image_subset_infs_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {b : α} :
      b tFinset.image (fun a => a b) s s t
      theorem Finset.image_subset_infs_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} :
      a sFinset.image (fun x => a x) t s t
      theorem Finset.forall_infs_iff {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {p : αProp} :
      ((c : α) → c s tp c) (a : α) → a s(b : α) → b tp (a b)
      @[simp]
      theorem Finset.infs_subset_iff {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {u : Finset α} :
      s t u ∀ (a : α), a s∀ (b : α), b ta b u
      @[simp]
      theorem Finset.empty_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {t : Finset α} :
      @[simp]
      theorem Finset.infs_empty {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :
      @[simp]
      theorem Finset.infs_eq_empty {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :
      s t = s = t =
      @[simp]
      theorem Finset.singleton_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {t : Finset α} {a : α} :
      {a} t = Finset.image (fun b => a b) t
      @[simp]
      theorem Finset.infs_singleton {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {b : α} :
      s {b} = Finset.image (fun a => a b) s
      theorem Finset.singleton_infs_singleton {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {a : α} {b : α} :
      {a} {b} = {a b}
      theorem Finset.infs_union_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
      (s₁ s₂) t = s₁ t s₂ t
      theorem Finset.infs_union_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
      s (t₁ t₂) = s t₁ s t₂
      theorem Finset.infs_inter_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
      (s₁ s₂) t s₁ t s₂ t
      theorem Finset.infs_inter_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
      s (t₁ t₂) s t₁ s t₂
      theorem Finset.subset_infs {α : Type u_1} [DecidableEq α] [SemilatticeInf α] {u : Finset α} {s : Set α} {t : Set α} :
      u s ts' t', s' s t' t u s' t'
      theorem Finset.biUnion_image_inf_left {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      (Finset.biUnion s fun a => Finset.image ((fun x x_1 => x x_1) a) t) = s t
      theorem Finset.biUnion_image_inf_right {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      (Finset.biUnion t fun b => Finset.image (fun a => a b) s) = s t
      theorem Finset.image_inf_product {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      Finset.image (Function.uncurry fun x x_1 => x x_1) (s ×ˢ t) = s t
      theorem Finset.infs_assoc {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s t u = s (t u)
      theorem Finset.infs_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      s t = t s
      theorem Finset.infs_left_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s (t u) = t (s u)
      theorem Finset.infs_right_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s t u = s u t
      theorem Finset.infs_infs_infs_comm {α : Type u_1} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :
      s t (u v) = s u (t v)
      theorem Finset.sups_infs_subset_left {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s t u (s t) (s u)
      theorem Finset.sups_infs_subset_right {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      t u s (t s) (u s)
      theorem Finset.infs_sups_subset_left {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s (t u) s t s u
      theorem Finset.infs_sups_subset_right {α : Type u_1} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      (t u) s t s u s
      def Finset.disjSups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :

      The finset of elements of the form a ⊔ b where a ∈ s, b ∈ t and a and b are disjoint.

      Instances For

        The finset of elements of the form a ⊔ b where a ∈ s, b ∈ t and a and b are disjoint.

        Instances For
          @[simp]
          theorem Finset.mem_disjSups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {c : α} :
          c Finset.disjSups s t a, a s b, b t Disjoint a b a b = c
          theorem Finset.disjSups_subset_sups {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :
          theorem Finset.disjSups_subset {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} (hs : s₁ s₂) (ht : t₁ t₂) :
          Finset.disjSups s₁ t₁ Finset.disjSups s₂ t₂
          theorem Finset.disjSups_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (ht : t₁ t₂) :
          theorem Finset.disjSups_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ s₂) :
          theorem Finset.forall_disjSups_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {p : αProp} :
          ((c : α) → c Finset.disjSups s tp c) (a : α) → a s(b : α) → b tDisjoint a bp (a b)
          @[simp]
          theorem Finset.disjSups_subset_iff {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {u : Finset α} :
          Finset.disjSups s t u ∀ (a : α), a s∀ (b : α), b tDisjoint a ba b u
          @[simp]
          @[simp]
          theorem Finset.disjSups_singleton {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {a : α} {b : α} :
          Finset.disjSups {a} {b} = if Disjoint a b then {a b} else
          theorem Finset.disjSups_union_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
          theorem Finset.disjSups_union_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
          theorem Finset.disjSups_inter_subset_left {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
          theorem Finset.disjSups_inter_subset_right {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
          theorem Finset.disjSups_comm {α : Type u_1} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :