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]

source

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

HasSups (Finset α)

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

Equations

Finset.hasSups = { sups := Finset.image₂ fun (x x_1 : α) => x ⊔ x_1 }

Instances For

source

@[simp]

theorem Finset.mem_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {c : α} :

c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c

source

@[simp]

theorem Finset.coe_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

↑(s ⊻ t) = ↑s ⊻ ↑t

source

theorem Finset.card_sups_le {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

(s ⊻ t).card ≤ s.card * t.card

source

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)

source

theorem Finset.sup_mem_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} {b : α} :

a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t

source

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₂

source

theorem Finset.sups_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂

source

theorem Finset.sups_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t

source

theorem Finset.image_subset_sups_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {b : α} :

b ∈ t → Finset.image (fun (x : α) => x ⊔ b) s ⊆ s ⊻ t

source

theorem Finset.image_subset_sups_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} :

a ∈ s → Finset.image (fun (x : α) => a ⊔ x) t ⊆ s ⊻ t

source

theorem Finset.forall_sups_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {p : α → Prop} :

(∀ c ∈ s ⊻ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊔ b)

source

@[simp]

theorem Finset.sups_subset_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} {u : Finset α} :

s ⊻ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊔ b ∈ u

source

@[simp]

theorem Finset.sups_nonempty {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

(s ⊻ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

source

theorem Finset.Nonempty.sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty

source

theorem Finset.Nonempty.of_sups_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

(s ⊻ t).Nonempty → s.Nonempty

source

theorem Finset.Nonempty.of_sups_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

(s ⊻ t).Nonempty → t.Nonempty

source

@[simp]

theorem Finset.empty_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {t : Finset α} :

∅ ⊻ t = ∅

source

@[simp]

theorem Finset.sups_empty {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :

s ⊻ ∅ = ∅

source

@[simp]

theorem Finset.sups_eq_empty {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t : Finset α} :

s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem Finset.singleton_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {t : Finset α} {a : α} :

{a} ⊻ t = Finset.image (fun (x : α) => a ⊔ x) t

source

@[simp]

theorem Finset.sups_singleton {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {b : α} :

s ⊻ {b} = Finset.image (fun (x : α) => x ⊔ b) s

source

theorem Finset.singleton_sups_singleton {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {a : α} {b : α} :

{a} ⊻ {b} = {a ⊔ b}

source

theorem Finset.sups_union_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t

source

theorem Finset.sups_union_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂

source

theorem Finset.sups_inter_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t

source

theorem Finset.sups_inter_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂

source

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'

source

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

source

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

source

theorem Finset.subset_sups_self {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :

s ⊆ s ⊻ s

source

theorem Finset.sups_subset_self {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :

s ⊻ s ⊆ s ↔ SupClosed ↑s

source

@[simp]

theorem Finset.sups_eq_self {α : Type u_2} [DecidableEq α] [SemilatticeSup α] {s : Finset α} :

s ⊻ s = s ↔ SupClosed ↑s

source

@[simp]

theorem Finset.univ_sups_univ {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [Fintype α] :

Finset.univ ⊻ Finset.univ = Finset.univ

source

theorem Finset.filter_sups_le {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (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

source

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

source

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

source

theorem Finset.image_sup_product {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

Finset.image (Function.uncurry fun (x x_1 : α) => x ⊔ x_1) (s ×ˢ t) = s ⊻ t

source

theorem Finset.sups_assoc {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ t ⊻ u = s ⊻ (t ⊻ u)

source

theorem Finset.sups_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) :

s ⊻ t = t ⊻ s

source

theorem Finset.sups_left_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)

source

theorem Finset.sups_right_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ t ⊻ u = s ⊻ u ⊻ t

source

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)

source

def Finset.hasInfs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] :

HasInfs (Finset α)

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

Equations

Finset.hasInfs = { infs := Finset.image₂ fun (x x_1 : α) => x ⊓ x_1 }

Instances For

source

@[simp]

theorem Finset.mem_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {c : α} :

c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c

source

@[simp]

theorem Finset.coe_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

↑(s ⊼ t) = ↑s ⊼ ↑t

source

theorem Finset.card_infs_le {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

(s ⊼ t).card ≤ s.card * t.card

source

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)

source

theorem Finset.inf_mem_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} {b : α} :

a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t

source

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₂

source

theorem Finset.infs_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂

source

theorem Finset.infs_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t

source

theorem Finset.image_subset_infs_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {b : α} :

b ∈ t → Finset.image (fun (x : α) => x ⊓ b) s ⊆ s ⊼ t

source

theorem Finset.image_subset_infs_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} :

a ∈ s → Finset.image (fun (x : α) => a ⊓ x) t ⊆ s ⊼ t

source

theorem Finset.forall_infs_iff {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {p : α → Prop} :

(∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b)

source

@[simp]

theorem Finset.infs_subset_iff {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} {u : Finset α} :

s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u

source

@[simp]

theorem Finset.infs_nonempty {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

(s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

source

theorem Finset.Nonempty.infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

s.Nonempty → t.Nonempty → (s ⊼ t).Nonempty

source

theorem Finset.Nonempty.of_infs_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

(s ⊼ t).Nonempty → s.Nonempty

source

theorem Finset.Nonempty.of_infs_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

(s ⊼ t).Nonempty → t.Nonempty

source

@[simp]

theorem Finset.empty_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {t : Finset α} :

∅ ⊼ t = ∅

source

@[simp]

theorem Finset.infs_empty {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :

s ⊼ ∅ = ∅

source

@[simp]

theorem Finset.infs_eq_empty {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t : Finset α} :

s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem Finset.singleton_infs {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {t : Finset α} {a : α} :

{a} ⊼ t = Finset.image (fun (x : α) => a ⊓ x) t

source

@[simp]

theorem Finset.infs_singleton {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {b : α} :

s ⊼ {b} = Finset.image (fun (x : α) => x ⊓ b) s

source

theorem Finset.singleton_infs_singleton {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {a : α} {b : α} :

{a} ⊼ {b} = {a ⊓ b}

source

theorem Finset.infs_union_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t

source

theorem Finset.infs_union_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂

source

theorem Finset.infs_inter_subset_left {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

(s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t

source

theorem Finset.infs_inter_subset_right {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂

source

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'

source

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

source

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

source

theorem Finset.subset_infs_self {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :

s ⊆ s ⊼ s

source

theorem Finset.infs_self_subset {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :

s ⊼ s ⊆ s ↔ InfClosed ↑s

source

@[simp]

theorem Finset.infs_self {α : Type u_2} [DecidableEq α] [SemilatticeInf α] {s : Finset α} :

s ⊼ s = s ↔ InfClosed ↑s

source

@[simp]

theorem Finset.univ_infs_univ {α : Type u_2} [DecidableEq α] [SemilatticeInf α] [Fintype α] :

Finset.univ ⊼ Finset.univ = Finset.univ

source

theorem Finset.filter_infs_le {α : Type u_2} [DecidableEq α] [SemilatticeInf α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (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

source

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

source

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

source

theorem Finset.image_inf_product {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

Finset.image (Function.uncurry fun (x x_1 : α) => x ⊓ x_1) (s ×ˢ t) = s ⊼ t

source

theorem Finset.infs_assoc {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ t ⊼ u = s ⊼ (t ⊼ u)

source

theorem Finset.infs_comm {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) :

s ⊼ t = t ⊼ s

source

theorem Finset.infs_left_comm {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)

source

theorem Finset.infs_right_comm {α : Type u_2} [DecidableEq α] [SemilatticeInf α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ t ⊼ u = s ⊼ u ⊼ t

source

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)

source

theorem Finset.sups_infs_subset_left {α : Type u_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)

source

theorem Finset.sups_infs_subset_right {α : Type u_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)

source

theorem Finset.infs_sups_subset_left {α : Type u_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u

source

theorem Finset.infs_sups_subset_right {α : Type u_2} [DecidableEq α] [DistribLattice α] (s : Finset α) (t : Finset α) (u : Finset α) :

(t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s

source

@[simp]

theorem Finset.powerset_union {α : Type u_2} [DecidableEq α] (s : Finset α) (t : Finset α) :

(s ∪ t).powerset = s.powerset ⊻ t.powerset

source

@[simp]

theorem Finset.powerset_inter {α : Type u_2} [DecidableEq α] (s : Finset α) (t : Finset α) :

(s ∩ t).powerset = s.powerset ⊼ t.powerset

source

@[simp]

theorem Finset.powerset_sups_powerset_self {α : Type u_2} [DecidableEq α] (s : Finset α) :

s.powerset ⊻ s.powerset = s.powerset

source

@[simp]

theorem Finset.powerset_infs_powerset_self {α : Type u_2} [DecidableEq α] (s : Finset α) :

s.powerset ⊼ s.powerset = s.powerset

source

theorem Finset.union_mem_sups {α : Type u_2} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : Finset α} {t : Finset α} :

s ∈ 𝒜 → t ∈ ℬ → s ∪ t ∈ 𝒜 ⊻ ℬ

source

theorem Finset.inter_mem_infs {α : Type u_2} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : Finset α} {t : Finset α} :

s ∈ 𝒜 → t ∈ ℬ → s ∩ t ∈ 𝒜 ⊼ ℬ

source

def Finset.disjSups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :

Finset α

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

Equations

s.disjSups t = Finset.image (fun (ab : α × α) => ab.1 ⊔ ab.2) (Finset.filter (fun (ab : α × α) => Disjoint ab.1 ab.2) (s ×ˢ t))

Instances For

source

def FinsetFamily.«term_○_» :

Lean.TrailingParserDescr

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

Equations

FinsetFamily.«term_○_» = Lean.ParserDescr.trailingNode `FinsetFamily.term_○_ 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ○ ") (Lean.ParserDescr.cat `term 75))

Instances For

source

@[simp]

theorem Finset.mem_disjSups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {c : α} :

c ∈ s.disjSups t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c

source

theorem Finset.disjSups_subset_sups {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :

s.disjSups t ⊆ s ⊻ t

source

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

source

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₂

source

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₂

source

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

source

theorem Finset.forall_disjSups_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {p : α → Prop} :

(∀ c ∈ s.disjSups t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

source

@[simp]

theorem Finset.disjSups_subset_iff {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} {u : Finset α} :

s.disjSups t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → a ⊔ b ∈ u

source

theorem Finset.Nonempty.of_disjSups_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :

(s.disjSups t).Nonempty → s.Nonempty

source

theorem Finset.Nonempty.of_disjSups_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} {t : Finset α} :

(s.disjSups t).Nonempty → t.Nonempty

source

@[simp]

theorem Finset.disjSups_empty_left {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {t : Finset α} :

∅.disjSups t = ∅

source

@[simp]

theorem Finset.disjSups_empty_right {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] {s : Finset α} :

s.disjSups ∅ = ∅

source

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 ∅

source

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

source

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₂

source

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

source

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₂

source

theorem Finset.disjSups_comm {α : Type u_2} [DecidableEq α] [SemilatticeSup α] [OrderBot α] [DecidableRel Disjoint] (s : Finset α) (t : Finset α) :

s.disjSups t = t.disjSups s

source

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)

source

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)

source

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

source

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)

source

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

Finset.diffs = Finset.image₂ fun (x x_1 : α) => x \ x_1

Instances For

source

def FinsetFamily.«term_\\_» :

Lean.TrailingParserDescr

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

Equations

FinsetFamily.«term_\\_» = Lean.ParserDescr.trailingNode `FinsetFamily.term_\\_ 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\\\ ") (Lean.ParserDescr.cat `term 75))

Instances For

source

@[simp]

theorem Finset.mem_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {c : α} :

c ∈ s.diffs t ↔ ∃ a ∈ s, ∃ b ∈ t, a \ b = c

source

@[simp]

theorem Finset.coe_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :

↑(s.diffs t) = Set.image2 (fun (x x_1 : α) => x \ x_1) ↑s ↑t

source

theorem Finset.card_diffs_le {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :

(s.diffs t).card ≤ s.card * t.card

source

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)

source

theorem Finset.sdiff_mem_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {a : α} {b : α} :

a ∈ s → b ∈ t → a \ b ∈ s.diffs t

source

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₂

source

theorem Finset.diffs_subset_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :

t₁ ⊆ t₂ → s.diffs t₁ ⊆ s.diffs t₂

source

theorem Finset.diffs_subset_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :

s₁ ⊆ s₂ → s₁.diffs t ⊆ s₂.diffs t

source

theorem Finset.image_subset_diffs_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {b : α} :

b ∈ t → Finset.image (fun (x : α) => x \ b) s ⊆ s.diffs t

source

theorem Finset.image_subset_diffs_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {a : α} :

a ∈ s → Finset.image (fun (x : α) => a \ x) t ⊆ s.diffs t

source

theorem Finset.forall_mem_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {p : α → Prop} :

(∀ c ∈ s.diffs t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a \ b)

source

@[simp]

theorem Finset.diffs_subset_iff {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} {u : Finset α} :

s.diffs t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a \ b ∈ u

source

@[simp]

theorem Finset.diffs_nonempty {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :

(s.diffs t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

source

theorem Finset.Nonempty.diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :

s.Nonempty → t.Nonempty → (s.diffs t).Nonempty

source

theorem Finset.Nonempty.of_diffs_left {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :

(s.diffs t).Nonempty → s.Nonempty

source

theorem Finset.Nonempty.of_diffs_right {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :

(s.diffs t).Nonempty → t.Nonempty

source

@[simp]

theorem Finset.empty_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {t : Finset α} :

∅.diffs t = ∅

source

@[simp]

theorem Finset.diffs_empty {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} :

s.diffs ∅ = ∅

source

@[simp]

theorem Finset.diffs_eq_empty {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {t : Finset α} :

s.diffs t = ∅ ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem Finset.singleton_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {t : Finset α} {a : α} :

{a}.diffs t = Finset.image (fun (x : α) => a \ x) t

source

@[simp]

theorem Finset.diffs_singleton {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {s : Finset α} {b : α} :

s.diffs {b} = Finset.image (fun (x : α) => x \ b) s

source

theorem Finset.singleton_diffs_singleton {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {a : α} {b : α} :

{a}.diffs {b} = {a \ b}

source

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

source

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₂

source

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

source

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₂

source

theorem Finset.subset_diffs {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] {u : Finset α} {s : Set α} {t : Set α} :

↑u ⊆ Set.image2 (fun (x x_1 : α) => x \ x_1) s t → ∃ (s' : Finset α) (t' : Finset α), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s'.diffs t'

source

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

source

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

source

theorem Finset.image_sdiff_product {α : Type u_2} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :

Finset.image (Function.uncurry fun (x x_1 : α) => x \ x_1) (s ×ˢ t) = s.diffs t

source

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

source

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

source

def FinsetFamily.«term_ᶜˢ» :

Lean.TrailingParserDescr

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

Equations

FinsetFamily.«term_ᶜˢ» = Lean.ParserDescr.trailingNode `FinsetFamily.term_ᶜˢ 1024 1024 (Lean.ParserDescr.symbol "ᶜˢ")

Instances For

source

@[simp]

theorem Finset.mem_compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {a : α} :

a ∈ s.compls ↔ aᶜ ∈ s

source

@[simp]

theorem Finset.image_compl {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) :

Finset.image compl s = s.compls

source

@[simp]

theorem Finset.coe_compls {α : Type u_2} [BooleanAlgebra α] (s : Finset α) :

↑s.compls = compl '' ↑s

source

@[simp]

theorem Finset.card_compls {α : Type u_2} [BooleanAlgebra α] (s : Finset α) :

s.compls.card = s.card

source

theorem Finset.compl_mem_compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {a : α} :

a ∈ s → aᶜ ∈ s.compls

source

@[simp]

theorem Finset.compls_subset_compls {α : Type u_2} [BooleanAlgebra α] {s₁ : Finset α} {s₂ : Finset α} :

s₁.compls ⊆ s₂.compls ↔ s₁ ⊆ s₂

source

theorem Finset.forall_mem_compls {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {p : α → Prop} :

(∀ a ∈ s.compls, p a) ↔ ∀ a ∈ s, p aᶜ

source

theorem Finset.exists_compls_iff {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {p : α → Prop} :

(∃ a ∈ s.compls, p a) ↔ ∃ a ∈ s, p aᶜ

source

@[simp]

theorem Finset.compls_compls {α : Type u_2} [BooleanAlgebra α] (s : Finset α) :

s.compls.compls = s

source

theorem Finset.compls_subset_iff {α : Type u_2} [BooleanAlgebra α] {s : Finset α} {t : Finset α} :

s.compls ⊆ t ↔ s ⊆ t.compls

source

@[simp]

theorem Finset.compls_nonempty {α : Type u_2} [BooleanAlgebra α] {s : Finset α} :

s.compls.Nonempty ↔ s.Nonempty

source

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

s.compls.Nonempty → s.Nonempty

Alias of the forward direction of Finset.compls_nonempty.

source

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

s.Nonempty → s.compls.Nonempty

Alias of the reverse direction of Finset.compls_nonempty.

source

@[simp]

theorem Finset.compls_empty {α : Type u_2} [BooleanAlgebra α] :

∅.compls = ∅

source

@[simp]

theorem Finset.compls_eq_empty {α : Type u_2} [BooleanAlgebra α] {s : Finset α} :

s.compls = ∅ ↔ s = ∅

source

@[simp]

theorem Finset.compls_singleton {α : Type u_2} [BooleanAlgebra α] (a : α) :

{a}.compls = {aᶜ}

source

@[simp]

theorem Finset.compls_univ {α : Type u_2} [BooleanAlgebra α] [Fintype α] :

Finset.univ.compls = Finset.univ

source

@[simp]

theorem Finset.compls_union {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) (t : Finset α) :

(s ∪ t).compls = s.compls ∪ t.compls

source

@[simp]

theorem Finset.compls_inter {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) (t : Finset α) :

(s ∩ t).compls = s.compls ∩ t.compls

source

@[simp]

theorem Finset.compls_infs {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) (t : Finset α) :

(s ⊼ t).compls = s.compls ⊻ t.compls

source

@[simp]

theorem Finset.compls_sups {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) (t : Finset α) :

(s ⊻ t).compls = s.compls ⊼ t.compls

source

@[simp]

theorem Finset.infs_compls_eq_diffs {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) (t : Finset α) :

s ⊼ t.compls = s.diffs t

source

@[simp]

theorem Finset.compls_infs_eq_diffs {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) (t : Finset α) :

s.compls ⊼ t = t.diffs s

source

@[simp]

theorem Finset.diffs_compls_eq_infs {α : Type u_2} [DecidableEq α] [BooleanAlgebra α] (s : Finset α) (t : Finset α) :

s.diffs t.compls = s ⊼ t

source

theorem Set.Sized.compls {α : Type u_2} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {n : ℕ} (h𝒜 : Set.Sized n ↑𝒜) :

Set.Sized (Fintype.card α - n) ↑𝒜.compls

source

theorem Finset.sized_compls {α : Type u_2} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {n : ℕ} (hn : n ≤ Fintype.card α) :

Set.Sized n ↑𝒜.compls ↔ Set.Sized (Fintype.card α - n) ↑𝒜

Documentation

Mathlib.Data.Finset.Sups

Set family operations #

Main declarations #

Notation #

References #