# Set family operations #

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

## Main declarations #

• Finset.sups s t: Finset of elements of the form a ⊔ b where a ∈ s, b ∈ t.
• Finset.infs s t: Finset of elements of the form a ⊓ b where a ∈ s, b ∈ t.
• Finset.disjSups s t: Finset of elements of the form a ⊔ b where a ∈ s, b ∈ t and a and b are disjoint.
• Finset.diffs: Finset of elements of the form a \ b where a ∈ s, b ∈ t.
• Finset.compls: Finset of elements of the form aᶜ where a ∈ s.

## Notation #

We define the following notation in locale FinsetFamily:

• s ⊻ t for Finset.sups
• s ⊼ t for Finset.infs
• s ○ t for Finset.disjSups s t
• s \\ t for Finset.diffs
• sᶜˢ for Finset.compls

## References #

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

def Finset.hasSups {α : Type u_2} [] [] :

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} [] [] {s : } {t : } {c : α} :
c s t as, bt, a b = c
@[simp]
theorem Finset.coe_sups {α : Type u_2} [] [] (s : ) (t : ) :
(s t) = s t
theorem Finset.card_sups_le {α : Type u_2} [] [] (s : ) (t : ) :
(s t).card s.card * t.card
theorem Finset.card_sups_iff {α : Type u_2} [] [] (s : ) (t : ) :
(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} [] [] {s : } {t : } {a : α} {b : α} :
a sb ta b s t
theorem Finset.sups_subset {α : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
theorem Finset.sups_subset_left {α : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
t₁ t₂s t₁ s t₂
theorem Finset.sups_subset_right {α : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ t s₂ t
theorem Finset.image_subset_sups_left {α : Type u_2} [] [] {s : } {t : } {b : α} :
b tFinset.image (fun (x : α) => x b) s s t
theorem Finset.image_subset_sups_right {α : Type u_2} [] [] {s : } {t : } {a : α} :
a sFinset.image (fun (x : α) => a x) t s t
theorem Finset.forall_sups_iff {α : Type u_2} [] [] {s : } {t : } {p : αProp} :
(cs t, p c) as, bt, p (a b)
@[simp]
theorem Finset.sups_subset_iff {α : Type u_2} [] [] {s : } {t : } {u : } :
s t u as, bt, a b u
@[simp]
theorem Finset.sups_nonempty {α : Type u_2} [] [] {s : } {t : } :
(s t).Nonempty s.Nonempty t.Nonempty
theorem Finset.Nonempty.sups {α : Type u_2} [] [] {s : } {t : } :
s.Nonemptyt.Nonempty(s t).Nonempty
theorem Finset.Nonempty.of_sups_left {α : Type u_2} [] [] {s : } {t : } :
(s t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_sups_right {α : Type u_2} [] [] {s : } {t : } :
(s t).Nonemptyt.Nonempty
@[simp]
theorem Finset.empty_sups {α : Type u_2} [] [] {t : } :
@[simp]
theorem Finset.sups_empty {α : Type u_2} [] [] {s : } :
@[simp]
theorem Finset.sups_eq_empty {α : Type u_2} [] [] {s : } {t : } :
s t = s = t =
@[simp]
theorem Finset.singleton_sups {α : Type u_2} [] [] {t : } {a : α} :
{a} t = Finset.image (fun (x : α) => a x) t
@[simp]
theorem Finset.sups_singleton {α : Type u_2} [] [] {s : } {b : α} :
s {b} = Finset.image (fun (x : α) => x b) s
theorem Finset.singleton_sups_singleton {α : Type u_2} [] [] {a : α} {b : α} :
{a} {b} = {a b}
theorem Finset.sups_union_left {α : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
(s₁ s₂) t = s₁ t s₂ t
theorem Finset.sups_union_right {α : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
s (t₁ t₂) = s t₁ s t₂
theorem Finset.sups_inter_subset_left {α : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
(s₁ s₂) t s₁ t s₂ t
theorem Finset.sups_inter_subset_right {α : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
s (t₁ t₂) s t₁ s t₂
theorem Finset.subset_sups {α : Type u_2} [] [] {u : } {s : Set α} {t : Set α} :
u s t∃ (s' : ) (t' : ), s' s t' t u s' t'
theorem Finset.image_sups {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [FunLike F α β] [SupHomClass F α β] (f : F) (s : ) (t : ) :
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} [] [] [] [] [FunLike F α β] [SupHomClass F α β] (f : F) (hf : ) (s : ) (t : ) :
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} [] [] {s : } :
s s s
theorem Finset.sups_subset_self {α : Type u_2} [] [] {s : } :
s s s
@[simp]
theorem Finset.sups_eq_self {α : Type u_2} [] [] {s : } :
s s = s
@[simp]
theorem Finset.univ_sups_univ {α : Type u_2} [] [] [] :
Finset.univ Finset.univ = Finset.univ
theorem Finset.filter_sups_le {α : Type u_2} [] [] [DecidableRel fun (x x_1 : α) => x x_1] (s : ) (t : ) (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} [] [] (s : ) (t : ) :
(s.biUnion fun (a : α) => Finset.image (fun (x : α) => a x) t) = s t
theorem Finset.biUnion_image_sup_right {α : Type u_2} [] [] (s : ) (t : ) :
(t.biUnion fun (b : α) => Finset.image (fun (x : α) => x b) s) = s t
theorem Finset.image_sup_product {α : Type u_2} [] [] (s : ) (t : ) :
Finset.image (Function.uncurry fun (x x_1 : α) => x x_1) (s ×ˢ t) = s t
theorem Finset.sups_assoc {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s t u = s (t u)
theorem Finset.sups_comm {α : Type u_2} [] [] (s : ) (t : ) :
s t = t s
theorem Finset.sups_left_comm {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s (t u) = t (s u)
theorem Finset.sups_right_comm {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s t u = s u t
theorem Finset.sups_sups_sups_comm {α : Type u_2} [] [] (s : ) (t : ) (u : ) (v : ) :
s t (u v) = s u (t v)
def Finset.hasInfs {α : Type u_2} [] [] :

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} [] [] {s : } {t : } {c : α} :
c s t as, bt, a b = c
@[simp]
theorem Finset.coe_infs {α : Type u_2} [] [] (s : ) (t : ) :
(s t) = s t
theorem Finset.card_infs_le {α : Type u_2} [] [] (s : ) (t : ) :
(s t).card s.card * t.card
theorem Finset.card_infs_iff {α : Type u_2} [] [] (s : ) (t : ) :
(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} [] [] {s : } {t : } {a : α} {b : α} :
a sb ta b s t
theorem Finset.infs_subset {α : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
theorem Finset.infs_subset_left {α : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
t₁ t₂s t₁ s t₂
theorem Finset.infs_subset_right {α : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ t s₂ t
theorem Finset.image_subset_infs_left {α : Type u_2} [] [] {s : } {t : } {b : α} :
b tFinset.image (fun (x : α) => x b) s s t
theorem Finset.image_subset_infs_right {α : Type u_2} [] [] {s : } {t : } {a : α} :
a sFinset.image (fun (x : α) => a x) t s t
theorem Finset.forall_infs_iff {α : Type u_2} [] [] {s : } {t : } {p : αProp} :
(cs t, p c) as, bt, p (a b)
@[simp]
theorem Finset.infs_subset_iff {α : Type u_2} [] [] {s : } {t : } {u : } :
s t u as, bt, a b u
@[simp]
theorem Finset.infs_nonempty {α : Type u_2} [] [] {s : } {t : } :
(s t).Nonempty s.Nonempty t.Nonempty
theorem Finset.Nonempty.infs {α : Type u_2} [] [] {s : } {t : } :
s.Nonemptyt.Nonempty(s t).Nonempty
theorem Finset.Nonempty.of_infs_left {α : Type u_2} [] [] {s : } {t : } :
(s t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_infs_right {α : Type u_2} [] [] {s : } {t : } :
(s t).Nonemptyt.Nonempty
@[simp]
theorem Finset.empty_infs {α : Type u_2} [] [] {t : } :
@[simp]
theorem Finset.infs_empty {α : Type u_2} [] [] {s : } :
@[simp]
theorem Finset.infs_eq_empty {α : Type u_2} [] [] {s : } {t : } :
s t = s = t =
@[simp]
theorem Finset.singleton_infs {α : Type u_2} [] [] {t : } {a : α} :
{a} t = Finset.image (fun (x : α) => a x) t
@[simp]
theorem Finset.infs_singleton {α : Type u_2} [] [] {s : } {b : α} :
s {b} = Finset.image (fun (x : α) => x b) s
theorem Finset.singleton_infs_singleton {α : Type u_2} [] [] {a : α} {b : α} :
{a} {b} = {a b}
theorem Finset.infs_union_left {α : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
(s₁ s₂) t = s₁ t s₂ t
theorem Finset.infs_union_right {α : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
s (t₁ t₂) = s t₁ s t₂
theorem Finset.infs_inter_subset_left {α : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
(s₁ s₂) t s₁ t s₂ t
theorem Finset.infs_inter_subset_right {α : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
s (t₁ t₂) s t₁ s t₂
theorem Finset.subset_infs {α : Type u_2} [] [] {u : } {s : Set α} {t : Set α} :
u s t∃ (s' : ) (t' : ), s' s t' t u s' t'
theorem Finset.image_infs {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [FunLike F α β] [InfHomClass F α β] (f : F) (s : ) (t : ) :
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} [] [] [] [] [FunLike F α β] [InfHomClass F α β] (f : F) (hf : ) (s : ) (t : ) :
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} [] [] {s : } :
s s s
theorem Finset.infs_self_subset {α : Type u_2} [] [] {s : } :
s s s
@[simp]
theorem Finset.infs_self {α : Type u_2} [] [] {s : } :
s s = s
@[simp]
theorem Finset.univ_infs_univ {α : Type u_2} [] [] [] :
Finset.univ Finset.univ = Finset.univ
theorem Finset.filter_infs_le {α : Type u_2} [] [] [DecidableRel fun (x x_1 : α) => x x_1] (s : ) (t : ) (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} [] [] (s : ) (t : ) :
(s.biUnion fun (a : α) => Finset.image (fun (x : α) => a x) t) = s t
theorem Finset.biUnion_image_inf_right {α : Type u_2} [] [] (s : ) (t : ) :
(t.biUnion fun (b : α) => Finset.image (fun (x : α) => x b) s) = s t
theorem Finset.image_inf_product {α : Type u_2} [] [] (s : ) (t : ) :
Finset.image (Function.uncurry fun (x x_1 : α) => x x_1) (s ×ˢ t) = s t
theorem Finset.infs_assoc {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s t u = s (t u)
theorem Finset.infs_comm {α : Type u_2} [] [] (s : ) (t : ) :
s t = t s
theorem Finset.infs_left_comm {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s (t u) = t (s u)
theorem Finset.infs_right_comm {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s t u = s u t
theorem Finset.infs_infs_infs_comm {α : Type u_2} [] [] (s : ) (t : ) (u : ) (v : ) :
s t (u v) = s u (t v)
theorem Finset.sups_infs_subset_left {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s t u (s t) (s u)
theorem Finset.sups_infs_subset_right {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
t u s (t s) (u s)
theorem Finset.infs_sups_subset_left {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
s (t u) s t s u
theorem Finset.infs_sups_subset_right {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
(t u) s t s u s
@[simp]
theorem Finset.powerset_union {α : Type u_2} [] (s : ) (t : ) :
(s t).powerset = s.powerset t.powerset
@[simp]
theorem Finset.powerset_inter {α : Type u_2} [] (s : ) (t : ) :
(s t).powerset = s.powerset t.powerset
@[simp]
theorem Finset.powerset_sups_powerset_self {α : Type u_2} [] (s : ) :
s.powerset s.powerset = s.powerset
@[simp]
theorem Finset.powerset_infs_powerset_self {α : Type u_2} [] (s : ) :
s.powerset s.powerset = s.powerset
theorem Finset.union_mem_sups {α : Type u_2} [] {𝒜 : Finset ()} {ℬ : Finset ()} {s : } {t : } :
s 𝒜t s t 𝒜
theorem Finset.inter_mem_infs {α : Type u_2} [] {𝒜 : Finset ()} {ℬ : Finset ()} {s : } {t : } :
s 𝒜t s t 𝒜
def Finset.disjSups {α : Type u_2} [] [] [] [DecidableRel Disjoint] (s : ) (t : ) :

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} [] [] [] [DecidableRel Disjoint] {s : } {t : } {c : α} :
c s.disjSups t as, bt, Disjoint a b a b = c
theorem Finset.disjSups_subset_sups {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t : } :
s.disjSups t s t
theorem Finset.card_disjSups_le {α : Type u_2} [] [] [] [DecidableRel Disjoint] (s : ) (t : ) :
(s.disjSups t).card s.card * t.card
theorem Finset.disjSups_subset {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.disjSups t₁ s₂.disjSups t₂
theorem Finset.disjSups_subset_left {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t₁ : } {t₂ : } (ht : t₁ t₂) :
s.disjSups t₁ s.disjSups t₂
theorem Finset.disjSups_subset_right {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s₁ : } {s₂ : } {t : } (hs : s₁ s₂) :
s₁.disjSups t s₂.disjSups t
theorem Finset.forall_disjSups_iff {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t : } {p : αProp} :
(cs.disjSups t, p c) as, bt, Disjoint a bp (a b)
@[simp]
theorem Finset.disjSups_subset_iff {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t : } {u : } :
s.disjSups t u as, bt, Disjoint a ba b u
theorem Finset.Nonempty.of_disjSups_left {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t : } :
(s.disjSups t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_disjSups_right {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t : } :
(s.disjSups t).Nonemptyt.Nonempty
@[simp]
theorem Finset.disjSups_empty_left {α : Type u_2} [] [] [] [DecidableRel Disjoint] {t : } :
.disjSups t =
@[simp]
theorem Finset.disjSups_empty_right {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } :
s.disjSups =
theorem Finset.disjSups_singleton {α : Type u_2} [] [] [] [DecidableRel Disjoint] {a : α} {b : α} :
{a}.disjSups {b} = if Disjoint a b then {a b} else
theorem Finset.disjSups_union_left {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s₁ : } {s₂ : } {t : } :
(s₁ s₂).disjSups t = s₁.disjSups t s₂.disjSups t
theorem Finset.disjSups_union_right {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t₁ : } {t₂ : } :
s.disjSups (t₁ t₂) = s.disjSups t₁ s.disjSups t₂
theorem Finset.disjSups_inter_subset_left {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s₁ : } {s₂ : } {t : } :
(s₁ s₂).disjSups t s₁.disjSups t s₂.disjSups t
theorem Finset.disjSups_inter_subset_right {α : Type u_2} [] [] [] [DecidableRel Disjoint] {s : } {t₁ : } {t₂ : } :
s.disjSups (t₁ t₂) s.disjSups t₁ s.disjSups t₂
theorem Finset.disjSups_comm {α : Type u_2} [] [] [] [DecidableRel Disjoint] (s : ) (t : ) :
s.disjSups t = t.disjSups s
theorem Finset.disjSups_assoc {α : Type u_2} [] [] [] [DecidableRel Disjoint] (s : ) (t : ) (u : ) :
(s.disjSups t).disjSups u = s.disjSups (t.disjSups u)
theorem Finset.disjSups_left_comm {α : Type u_2} [] [] [] [DecidableRel Disjoint] (s : ) (t : ) (u : ) :
s.disjSups (t.disjSups u) = t.disjSups (s.disjSups u)
theorem Finset.disjSups_right_comm {α : Type u_2} [] [] [] [DecidableRel Disjoint] (s : ) (t : ) (u : ) :
(s.disjSups t).disjSups u = (s.disjSups u).disjSups t
theorem Finset.disjSups_disjSups_disjSups_comm {α : Type u_2} [] [] [] [DecidableRel Disjoint] (s : ) (t : ) (u : ) (v : ) :
(s.disjSups t).disjSups (u.disjSups v) = (s.disjSups u).disjSups (t.disjSups v)
def Finset.diffs {α : Type u_2} [] :

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} [] {s : } {t : } {c : α} :
c s.diffs t as, bt, a \ b = c
@[simp]
theorem Finset.coe_diffs {α : Type u_2} [] (s : ) (t : ) :
(s.diffs t) = Set.image2 (fun (x x_1 : α) => x \ x_1) s t
theorem Finset.card_diffs_le {α : Type u_2} [] (s : ) (t : ) :
(s.diffs t).card s.card * t.card
theorem Finset.card_diffs_iff {α : Type u_2} [] (s : ) (t : ) :
(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} [] {s : } {t : } {a : α} {b : α} :
a sb ta \ b s.diffs t
theorem Finset.diffs_subset {α : Type u_2} [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁.diffs t₁ s₂.diffs t₂
theorem Finset.diffs_subset_left {α : Type u_2} [] {s : } {t₁ : } {t₂ : } :
t₁ t₂s.diffs t₁ s.diffs t₂
theorem Finset.diffs_subset_right {α : Type u_2} [] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁.diffs t s₂.diffs t
theorem Finset.image_subset_diffs_left {α : Type u_2} [] {s : } {t : } {b : α} :
b tFinset.image (fun (x : α) => x \ b) s s.diffs t
theorem Finset.image_subset_diffs_right {α : Type u_2} [] {s : } {t : } {a : α} :
a sFinset.image (fun (x : α) => a \ x) t s.diffs t
theorem Finset.forall_mem_diffs {α : Type u_2} [] {s : } {t : } {p : αProp} :
(cs.diffs t, p c) as, bt, p (a \ b)
@[simp]
theorem Finset.diffs_subset_iff {α : Type u_2} [] {s : } {t : } {u : } :
s.diffs t u as, bt, a \ b u
@[simp]
theorem Finset.diffs_nonempty {α : Type u_2} [] {s : } {t : } :
(s.diffs t).Nonempty s.Nonempty t.Nonempty
theorem Finset.Nonempty.diffs {α : Type u_2} [] {s : } {t : } :
s.Nonemptyt.Nonempty(s.diffs t).Nonempty
theorem Finset.Nonempty.of_diffs_left {α : Type u_2} [] {s : } {t : } :
(s.diffs t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_diffs_right {α : Type u_2} [] {s : } {t : } :
(s.diffs t).Nonemptyt.Nonempty
@[simp]
theorem Finset.empty_diffs {α : Type u_2} [] {t : } :
.diffs t =
@[simp]
theorem Finset.diffs_empty {α : Type u_2} [] {s : } :
s.diffs =
@[simp]
theorem Finset.diffs_eq_empty {α : Type u_2} [] {s : } {t : } :
s.diffs t = s = t =
@[simp]
theorem Finset.singleton_diffs {α : Type u_2} [] {t : } {a : α} :
{a}.diffs t = Finset.image (fun (x : α) => a \ x) t
@[simp]
theorem Finset.diffs_singleton {α : Type u_2} [] {s : } {b : α} :
s.diffs {b} = Finset.image (fun (x : α) => x \ b) s
theorem Finset.singleton_diffs_singleton {α : Type u_2} [] {a : α} {b : α} :
{a}.diffs {b} = {a \ b}
theorem Finset.diffs_union_left {α : Type u_2} [] {s₁ : } {s₂ : } {t : } :
(s₁ s₂).diffs t = s₁.diffs t s₂.diffs t
theorem Finset.diffs_union_right {α : Type u_2} [] {s : } {t₁ : } {t₂ : } :
s.diffs (t₁ t₂) = s.diffs t₁ s.diffs t₂
theorem Finset.diffs_inter_subset_left {α : Type u_2} [] {s₁ : } {s₂ : } {t : } :
(s₁ s₂).diffs t s₁.diffs t s₂.diffs t
theorem Finset.diffs_inter_subset_right {α : Type u_2} [] {s : } {t₁ : } {t₂ : } :
s.diffs (t₁ t₂) s.diffs t₁ s.diffs t₂
theorem Finset.subset_diffs {α : Type u_2} [] {u : } {s : Set α} {t : Set α} :
u Set.image2 (fun (x x_1 : α) => x \ x_1) s t∃ (s' : ) (t' : ), s' s t' t u s'.diffs t'
theorem Finset.biUnion_image_sdiff_left {α : Type u_2} [] (s : ) (t : ) :
(s.biUnion fun (a : α) => Finset.image (fun (x : α) => a \ x) t) = s.diffs t
theorem Finset.biUnion_image_sdiff_right {α : Type u_2} [] (s : ) (t : ) :
(t.biUnion fun (b : α) => Finset.image (fun (x : α) => x \ b) s) = s.diffs t
theorem Finset.image_sdiff_product {α : Type u_2} [] (s : ) (t : ) :
Finset.image (Function.uncurry fun (x x_1 : α) => x \ x_1) (s ×ˢ t) = s.diffs t
theorem Finset.diffs_right_comm {α : Type u_2} [] (s : ) (t : ) (u : ) :
(s.diffs t).diffs u = (s.diffs u).diffs t
def Finset.compls {α : Type u_2} [] :

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} [] {s : } {a : α} :
a s.compls a s
@[simp]
theorem Finset.image_compl {α : Type u_2} [] [] (s : ) :
Finset.image compl s = s.compls
@[simp]
theorem Finset.coe_compls {α : Type u_2} [] (s : ) :
s.compls = compl '' s
@[simp]
theorem Finset.card_compls {α : Type u_2} [] (s : ) :
s.compls.card = s.card
theorem Finset.compl_mem_compls {α : Type u_2} [] {s : } {a : α} :
a sa s.compls
@[simp]
theorem Finset.compls_subset_compls {α : Type u_2} [] {s₁ : } {s₂ : } :
s₁.compls s₂.compls s₁ s₂
theorem Finset.forall_mem_compls {α : Type u_2} [] {s : } {p : αProp} :
(as.compls, p a) as, p a
theorem Finset.exists_compls_iff {α : Type u_2} [] {s : } {p : αProp} :
(as.compls, p a) as, p a
@[simp]
theorem Finset.compls_compls {α : Type u_2} [] (s : ) :
s.compls.compls = s
theorem Finset.compls_subset_iff {α : Type u_2} [] {s : } {t : } :
s.compls t s t.compls
@[simp]
theorem Finset.compls_nonempty {α : Type u_2} [] {s : } :
s.compls.Nonempty s.Nonempty
theorem Finset.Nonempty.of_compls {α : Type u_2} [] {s : } :
s.compls.Nonemptys.Nonempty

Alias of the forward direction of Finset.compls_nonempty.

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

Alias of the reverse direction of Finset.compls_nonempty.

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