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

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

Equations
Instances For
    @[simp]
    theorem Finset.mem_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {c : α} :
    c s t as, bt, a b = c
    @[simp]
    theorem Finset.coe_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    (s t) = s t
    theorem Finset.card_sups_le {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    (s t).card s.card * t.card
    theorem Finset.card_sups_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    (s t).card = s.card * t.card Set.InjOn (fun (x : α × α) => x.1 x.2) (s ×ˢ t)
    theorem Finset.sup_mem_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
    a sb ta b s t
    theorem Finset.sups_subset {α : Type u_2} [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_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
    t₁ t₂s t₁ s t₂
    theorem Finset.sups_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
    s₁ s₂s₁ t s₂ t
    theorem Finset.image_subset_sups_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {b : α} :
    b tFinset.image (fun (x : α) => x b) s s t
    theorem Finset.image_subset_sups_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} :
    a sFinset.image (fun (x : α) => a x) t s t
    theorem Finset.forall_sups_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {p : αProp} :
    (∀ cs t, p c) as, bt, p (a b)
    @[simp]
    theorem Finset.sups_subset_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {u : Finset α} :
    s t u as, bt, a b u
    @[simp]
    theorem Finset.sups_nonempty {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :
    (s t).Nonempty s.Nonempty t.Nonempty
    theorem Finset.Nonempty.sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :
    s.Nonemptyt.Nonempty(s t).Nonempty
    theorem Finset.Nonempty.of_sups_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :
    (s t).Nonemptys.Nonempty
    theorem Finset.Nonempty.of_sups_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :
    (s t).Nonemptyt.Nonempty
    @[simp]
    theorem Finset.empty_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {t : Finset α} :
    @[simp]
    theorem Finset.sups_empty {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :
    @[simp]
    theorem Finset.sups_eq_empty {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :
    s t = s = t =
    @[simp]
    theorem Finset.singleton_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {t : Finset α} {a : α} :
    {a} t = Finset.image (fun (x : α) => a x) t
    @[simp]
    theorem Finset.sups_singleton {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {b : α} :
    s {b} = Finset.image (fun (x : α) => x b) s
    theorem Finset.singleton_sups_singleton {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {a : α} {b : α} :
    {a} {b} = {a b}
    theorem Finset.sups_union_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
    (s₁ s₂) t = s₁ t s₂ t
    theorem Finset.sups_union_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
    s (t₁ t₂) = s t₁ s t₂
    theorem Finset.sups_inter_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
    (s₁ s₂) t s₁ t s₂ t
    theorem Finset.sups_inter_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
    s (t₁ t₂) s t₁ s t₂
    theorem Finset.subset_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {u : Finset α} {s : Set α} {t : Set α} :
    u s t∃ (s' : Finset α) (t' : Finset α), s' s t' t u s' t'
    theorem Finset.image_sups {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) (s : Finset α) (t : Finset α) :
    Finset.image (⇑f) (s t) = Finset.image (⇑f) s Finset.image (⇑f) t
    theorem Finset.map_sups {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) (hf : Function.Injective f) (s : Finset α) (t : Finset α) :
    Finset.map { toFun := f, inj' := hf } (s t) = Finset.map { toFun := f, inj' := hf } s Finset.map { toFun := f, inj' := hf } t
    theorem Finset.subset_sups_self {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :
    s s s
    theorem Finset.sups_subset_self {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :
    s s s SupClosed s
    @[simp]
    theorem Finset.sups_eq_self {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :
    s s = s SupClosed s
    @[simp]
    theorem Finset.univ_sups_univ {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [Fintype α] :
    Finset.univ Finset.univ = Finset.univ
    theorem Finset.filter_sups_le {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [DecidableRel fun (x1 x2 : α) => x1 x2] (s : Finset α) (t : Finset α) (a : α) :
    Finset.filter (fun (x : α) => x a) (s t) = Finset.filter (fun (x : α) => x a) s Finset.filter (fun (x : α) => x a) t
    theorem Finset.biUnion_image_sup_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    (s.biUnion fun (a : α) => Finset.image (fun (x : α) => a x) t) = s t
    theorem Finset.biUnion_image_sup_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    (t.biUnion fun (b : α) => Finset.image (fun (x : α) => x b) s) = s t
    theorem Finset.image_sup_product {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    Finset.image (Function.uncurry fun (x1 x2 : α) => x1 x2) (s ×ˢ t) = s t
    theorem Finset.sups_assoc {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :
    s t u = s (t u)
    theorem Finset.sups_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :
    s t = t s
    theorem Finset.sups_left_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :
    s (t u) = t (s u)
    theorem Finset.sups_right_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :
    s t u = s u t
    theorem Finset.sups_sups_sups_comm {α : Type u_2} [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.

    Equations
    Instances For
      @[simp]
      theorem Finset.mem_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {c : α} :
      c s t as, bt, a b = c
      @[simp]
      theorem Finset.coe_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      (s t) = s t
      theorem Finset.card_infs_le {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      (s t).card s.card * t.card
      theorem Finset.card_infs_iff {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      (s t).card = s.card * t.card Set.InjOn (fun (x : α × α) => x.1 x.2) (s ×ˢ t)
      theorem Finset.inf_mem_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
      a sb ta b s t
      theorem Finset.infs_subset {α : Type u_2} [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_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
      t₁ t₂s t₁ s t₂
      theorem Finset.infs_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
      s₁ s₂s₁ t s₂ t
      theorem Finset.image_subset_infs_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {b : α} :
      b tFinset.image (fun (x : α) => x b) s s t
      theorem Finset.image_subset_infs_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} :
      a sFinset.image (fun (x : α) => a x) t s t
      theorem Finset.forall_infs_iff {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {p : αProp} :
      (∀ cs t, p c) as, bt, p (a b)
      @[simp]
      theorem Finset.infs_subset_iff {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {u : Finset α} :
      s t u as, bt, a b u
      @[simp]
      theorem Finset.infs_nonempty {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :
      (s t).Nonempty s.Nonempty t.Nonempty
      theorem Finset.Nonempty.infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :
      s.Nonemptyt.Nonempty(s t).Nonempty
      theorem Finset.Nonempty.of_infs_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :
      (s t).Nonemptys.Nonempty
      theorem Finset.Nonempty.of_infs_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :
      (s t).Nonemptyt.Nonempty
      @[simp]
      theorem Finset.empty_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {t : Finset α} :
      @[simp]
      theorem Finset.infs_empty {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :
      @[simp]
      theorem Finset.infs_eq_empty {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :
      s t = s = t =
      @[simp]
      theorem Finset.singleton_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {t : Finset α} {a : α} :
      {a} t = Finset.image (fun (x : α) => a x) t
      @[simp]
      theorem Finset.infs_singleton {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {b : α} :
      s {b} = Finset.image (fun (x : α) => x b) s
      theorem Finset.singleton_infs_singleton {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {a : α} {b : α} :
      {a} {b} = {a b}
      theorem Finset.infs_union_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
      (s₁ s₂) t = s₁ t s₂ t
      theorem Finset.infs_union_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
      s (t₁ t₂) = s t₁ s t₂
      theorem Finset.infs_inter_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
      (s₁ s₂) t s₁ t s₂ t
      theorem Finset.infs_inter_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
      s (t₁ t₂) s t₁ s t₂
      theorem Finset.subset_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {u : Finset α} {s : Set α} {t : Set α} :
      u s t∃ (s' : Finset α) (t' : Finset α), s' s t' t u s' t'
      theorem Finset.image_infs {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) (s : Finset α) (t : Finset α) :
      Finset.image (⇑f) (s t) = Finset.image (⇑f) s Finset.image (⇑f) t
      theorem Finset.map_infs {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) (hf : Function.Injective f) (s : Finset α) (t : Finset α) :
      Finset.map { toFun := f, inj' := hf } (s t) = Finset.map { toFun := f, inj' := hf } s Finset.map { toFun := f, inj' := hf } t
      theorem Finset.subset_infs_self {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :
      s s s
      theorem Finset.infs_self_subset {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :
      s s s InfClosed s
      @[simp]
      theorem Finset.infs_self {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :
      s s = s InfClosed s
      @[simp]
      theorem Finset.univ_infs_univ {α : Type u_2} [DecidableEq α] [SemilatticeInf α] [Fintype α] :
      Finset.univ Finset.univ = Finset.univ
      theorem Finset.filter_infs_le {α : Type u_2} [DecidableEq α] [SemilatticeInf α] [DecidableRel fun (x1 x2 : α) => x1 x2] (s : Finset α) (t : Finset α) (a : α) :
      Finset.filter (fun (x : α) => a x) (s t) = Finset.filter (fun (x : α) => a x) s Finset.filter (fun (x : α) => a x) t
      theorem Finset.biUnion_image_inf_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      (s.biUnion fun (a : α) => Finset.image (fun (x : α) => a x) t) = s t
      theorem Finset.biUnion_image_inf_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      (t.biUnion fun (b : α) => Finset.image (fun (x : α) => x b) s) = s t
      theorem Finset.image_inf_product {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      Finset.image (Function.uncurry fun (x1 x2 : α) => x1 x2) (s ×ˢ t) = s t
      theorem Finset.infs_assoc {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s t u = s (t u)
      theorem Finset.infs_comm {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :
      s t = t s
      theorem Finset.infs_left_comm {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s (t u) = t (s u)
      theorem Finset.infs_right_comm {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s t u = s u t
      theorem Finset.infs_infs_infs_comm {α : Type u_2} [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_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s t u (s t) (s u)
      theorem Finset.sups_infs_subset_right {α : Type u_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      t u s (t s) (u s)
      theorem Finset.infs_sups_subset_left {α : Type u_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      s (t u) s t s u
      theorem Finset.infs_sups_subset_right {α : Type u_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :
      (t u) s t s u s
      @[simp]
      theorem Finset.powerset_union {α : Type u_2} [DecidableEq α] (s : Finset α) (t : Finset α) :
      (s t).powerset = s.powerset t.powerset
      @[simp]
      theorem Finset.powerset_inter {α : Type u_2} [DecidableEq α] (s : Finset α) (t : Finset α) :
      (s t).powerset = s.powerset t.powerset
      @[simp]
      theorem Finset.powerset_sups_powerset_self {α : Type u_2} [DecidableEq α] (s : Finset α) :
      s.powerset s.powerset = s.powerset
      @[simp]
      theorem Finset.powerset_infs_powerset_self {α : Type u_2} [DecidableEq α] (s : Finset α) :
      s.powerset s.powerset = s.powerset
      theorem Finset.union_mem_sups {α : Type u_2} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : Finset α} {t : Finset α} :
      s 𝒜t s t 𝒜
      theorem Finset.inter_mem_infs {α : Type u_2} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : Finset α} {t : Finset α} :
      s 𝒜t s t 𝒜
      def Finset.disjSups {α : Type u_2} [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.

      Equations
      Instances For

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

        Equations
        Instances For
          @[simp]
          theorem Finset.mem_disjSups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {c : α} :
          c s.disjSups t as, bt, Disjoint a b a b = c
          theorem Finset.disjSups_subset_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :
          s.disjSups t s t
          theorem Finset.card_disjSups_le {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :
          (s.disjSups t).card s.card * t.card
          theorem Finset.disjSups_subset {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} (hs : s₁ s₂) (ht : t₁ t₂) :
          s₁.disjSups t₁ s₂.disjSups t₂
          theorem Finset.disjSups_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (ht : t₁ t₂) :
          s.disjSups t₁ s.disjSups t₂
          theorem Finset.disjSups_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ s₂) :
          s₁.disjSups t s₂.disjSups t
          theorem Finset.forall_disjSups_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {p : αProp} :
          (∀ cs.disjSups t, p c) as, bt, Disjoint a bp (a b)
          @[simp]
          theorem Finset.disjSups_subset_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {u : Finset α} :
          s.disjSups t u as, bt, Disjoint a ba b u
          theorem Finset.Nonempty.of_disjSups_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :
          (s.disjSups t).Nonemptys.Nonempty
          theorem Finset.Nonempty.of_disjSups_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :
          (s.disjSups t).Nonemptyt.Nonempty
          @[simp]
          theorem Finset.disjSups_empty_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {t : Finset α} :
          .disjSups t =
          @[simp]
          theorem Finset.disjSups_empty_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} :
          s.disjSups =
          theorem Finset.disjSups_singleton {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {a : α} {b : α} :
          {a}.disjSups {b} = if Disjoint a b then {a b} else
          theorem Finset.disjSups_union_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
          (s₁ s₂).disjSups t = s₁.disjSups t s₂.disjSups t
          theorem Finset.disjSups_union_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
          s.disjSups (t₁ t₂) = s.disjSups t₁ s.disjSups t₂
          theorem Finset.disjSups_inter_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
          (s₁ s₂).disjSups t s₁.disjSups t s₂.disjSups t
          theorem Finset.disjSups_inter_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
          s.disjSups (t₁ t₂) s.disjSups t₁ s.disjSups t₂
          theorem Finset.disjSups_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :
          s.disjSups t = t.disjSups s
          instance Finset.instCommutativeDisjSups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] :
          Std.Commutative fun (x1 x2 : Finset α) => x1.disjSups x2
          Equations
          • =
          theorem Finset.disjSups_assoc {α : Type u_2} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) :
          (s.disjSups t).disjSups u = s.disjSups (t.disjSups u)
          instance Finset.instAssociativeDisjSups {α : Type u_2} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] :
          Std.Associative fun (x1 x2 : Finset α) => x1.disjSups x2
          Equations
          • =
          theorem Finset.disjSups_left_comm {α : Type u_2} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) :
          s.disjSups (t.disjSups u) = t.disjSups (s.disjSups u)
          theorem Finset.disjSups_right_comm {α : Type u_2} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) :
          (s.disjSups t).disjSups u = (s.disjSups u).disjSups t
          theorem Finset.disjSups_disjSups_disjSups_comm {α : Type u_2} [DecidableEq α] [DistribLattice α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :
          (s.disjSups t).disjSups (u.disjSups v) = (s.disjSups u).disjSups (t.disjSups v)
          def Finset.diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] :
          Finset αFinset αFinset α

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

          Equations
          Instances For

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

            Equations
            Instances For
              @[simp]
              theorem Finset.mem_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {c : α} :
              c s.diffs t as, bt, a \ b = c
              @[simp]
              theorem Finset.coe_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :
              (s.diffs t) = Set.image2 (fun (x1 x2 : α) => x1 \ x2) s t
              theorem Finset.card_diffs_le {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :
              (s.diffs t).card s.card * t.card
              theorem Finset.card_diffs_iff {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :
              (s.diffs t).card = s.card * t.card Set.InjOn (fun (x : α × α) => x.1 \ x.2) (s ×ˢ t)
              theorem Finset.sdiff_mem_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
              a sb ta \ b s.diffs t
              theorem Finset.diffs_subset {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
              s₁ s₂t₁ t₂s₁.diffs t₁ s₂.diffs t₂
              theorem Finset.diffs_subset_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
              t₁ t₂s.diffs t₁ s.diffs t₂
              theorem Finset.diffs_subset_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
              s₁ s₂s₁.diffs t s₂.diffs t
              theorem Finset.image_subset_diffs_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {b : α} :
              b tFinset.image (fun (x : α) => x \ b) s s.diffs t
              theorem Finset.image_subset_diffs_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {a : α} :
              a sFinset.image (fun (x : α) => a \ x) t s.diffs t
              theorem Finset.forall_mem_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {p : αProp} :
              (∀ cs.diffs t, p c) as, bt, p (a \ b)
              @[simp]
              theorem Finset.diffs_subset_iff {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {u : Finset α} :
              s.diffs t u as, bt, a \ b u
              @[simp]
              theorem Finset.diffs_nonempty {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :
              (s.diffs t).Nonempty s.Nonempty t.Nonempty
              theorem Finset.Nonempty.diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :
              s.Nonemptyt.Nonempty(s.diffs t).Nonempty
              theorem Finset.Nonempty.of_diffs_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :
              (s.diffs t).Nonemptys.Nonempty
              theorem Finset.Nonempty.of_diffs_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :
              (s.diffs t).Nonemptyt.Nonempty
              @[simp]
              theorem Finset.empty_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {t : Finset α} :
              .diffs t =
              @[simp]
              theorem Finset.diffs_empty {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} :
              s.diffs =
              @[simp]
              theorem Finset.diffs_eq_empty {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :
              s.diffs t = s = t =
              @[simp]
              theorem Finset.singleton_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {t : Finset α} {a : α} :
              {a}.diffs t = Finset.image (fun (x : α) => a \ x) t
              @[simp]
              theorem Finset.diffs_singleton {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {b : α} :
              s.diffs {b} = Finset.image (fun (x : α) => x \ b) s
              theorem Finset.singleton_diffs_singleton {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {a : α} {b : α} :
              {a}.diffs {b} = {a \ b}
              theorem Finset.diffs_union_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
              (s₁ s₂).diffs t = s₁.diffs t s₂.diffs t
              theorem Finset.diffs_union_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
              s.diffs (t₁ t₂) = s.diffs t₁ s.diffs t₂
              theorem Finset.diffs_inter_subset_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
              (s₁ s₂).diffs t s₁.diffs t s₂.diffs t
              theorem Finset.diffs_inter_subset_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
              s.diffs (t₁ t₂) s.diffs t₁ s.diffs t₂
              theorem Finset.subset_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {u : Finset α} {s : Set α} {t : Set α} :
              u Set.image2 (fun (x1 x2 : α) => x1 \ x2) s t∃ (s' : Finset α) (t' : Finset α), s' s t' t u s'.diffs t'
              theorem Finset.biUnion_image_sdiff_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :
              (s.biUnion fun (a : α) => Finset.image (fun (x : α) => a \ x) t) = s.diffs t
              theorem Finset.biUnion_image_sdiff_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :
              (t.biUnion fun (b : α) => Finset.image (fun (x : α) => x \ b) s) = s.diffs t
              theorem Finset.image_sdiff_product {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :
              Finset.image (Function.uncurry fun (x1 x2 : α) => x1 \ x2) (s ×ˢ t) = s.diffs t
              theorem Finset.diffs_right_comm {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) (u : Finset α) :
              (s.diffs t).diffs u = (s.diffs u).diffs t
              def Finset.compls {α : Type u_2} [BooleanAlgebra α] :
              Finset αFinset α

              sᶜˢ is the finset of elements of the form aᶜ where a ∈ s.

              Equations
              • Finset.compls = Finset.map { toFun := compl, inj' := }
              Instances For

                sᶜˢ is the finset of elements of the form aᶜ where a ∈ s.

                Equations
                Instances For
                  @[simp]
                  theorem Finset.mem_compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {a : α} :
                  a s.compls a s
                  @[simp]
                  theorem Finset.image_compl {α : Type u_2} [BooleanAlgebra α] (s : Finset α) [DecidableEq α] :
                  Finset.image compl s = s.compls
                  @[simp]
                  theorem Finset.coe_compls {α : Type u_2} [BooleanAlgebra α] (s : Finset α) :
                  s.compls = compl '' s
                  @[simp]
                  theorem Finset.card_compls {α : Type u_2} [BooleanAlgebra α] (s : Finset α) :
                  s.compls.card = s.card
                  theorem Finset.compl_mem_compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {a : α} :
                  a sa s.compls
                  @[simp]
                  theorem Finset.compls_subset_compls {α : Type u_2} [BooleanAlgebra α] {s₁ : Finset α} {s₂ : Finset α} :
                  s₁.compls s₂.compls s₁ s₂
                  theorem Finset.forall_mem_compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {p : αProp} :
                  (∀ as.compls, p a) as, p a
                  theorem Finset.exists_compls_iff {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {p : αProp} :
                  (∃ as.compls, p a) as, p a
                  @[simp]
                  theorem Finset.compls_compls {α : Type u_2} [BooleanAlgebra α] (s : Finset α) :
                  s.compls.compls = s
                  theorem Finset.compls_subset_iff {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {t : Finset α} :
                  s.compls t s t.compls
                  @[simp]
                  theorem Finset.compls_nonempty {α : Type u_2} [BooleanAlgebra α] {s : Finset α} :
                  s.compls.Nonempty s.Nonempty
                  theorem Finset.Nonempty.compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} :
                  s.Nonemptys.compls.Nonempty

                  Alias of the reverse direction of Finset.compls_nonempty.

                  theorem Finset.Nonempty.of_compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} :
                  s.compls.Nonemptys.Nonempty

                  Alias of the forward direction of Finset.compls_nonempty.

                  @[simp]
                  theorem Finset.compls_empty {α : Type u_2} [BooleanAlgebra α] :
                  .compls =
                  @[simp]
                  theorem Finset.compls_eq_empty {α : Type u_2} [BooleanAlgebra α] {s : Finset α} :
                  s.compls = s =
                  @[simp]
                  theorem Finset.compls_singleton {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  {a}.compls = {a}
                  @[simp]
                  theorem Finset.compls_univ {α : Type u_2} [BooleanAlgebra α] [Fintype α] :
                  Finset.univ.compls = Finset.univ
                  @[simp]
                  theorem Finset.compls_union {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                  (s t).compls = s.compls t.compls
                  @[simp]
                  theorem Finset.compls_inter {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                  (s t).compls = s.compls t.compls
                  @[simp]
                  theorem Finset.compls_infs {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                  (s t).compls = s.compls t.compls
                  @[simp]
                  theorem Finset.compls_sups {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                  (s t).compls = s.compls t.compls
                  @[simp]
                  theorem Finset.infs_compls_eq_diffs {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                  s t.compls = s.diffs t
                  @[simp]
                  theorem Finset.compls_infs_eq_diffs {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                  s.compls t = t.diffs s
                  @[simp]
                  theorem Finset.diffs_compls_eq_infs {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                  s.diffs t.compls = s t
                  theorem Set.Sized.compls {α : Type u_4} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {n : } (h𝒜 : Set.Sized n 𝒜) :
                  Set.Sized (Fintype.card α - n) 𝒜.compls
                  theorem Finset.sized_compls {α : Type u_4} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {n : } (hn : n Fintype.card α) :
                  Set.Sized n 𝒜.compls Set.Sized (Fintype.card α - n) 𝒜