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.

Equations
@[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
@[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

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

Equations
@[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

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

Equations
@[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' := }

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

Equations
@[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) 𝒜