mathlib documentation

data.finset.lattice

Lattice operations on finsets

sup

source
def finset.sup {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] (s : finset β) (f : β → α) :
α

Supremum of a finite set: sup {a, b, c} f = f a ⊔ f b ⊔ f c

Equations
source
theorem finset.sup_def {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f : β → α} :
s.sup f = (multiset.map f s.val).sup

source
@[simp]
theorem finset.sup_empty {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {f : β → α} :
∅.sup f = ⊥

source
@[simp]
theorem finset.sup_insert {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).sup f = f b ⊔ s.sup f

source
@[simp]
theorem finset.sup_singleton {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {f : β → α} {b : β} :
{b}.sup f = f b

source
theorem finset.sup_union {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f

source
theorem finset.sup_congr {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (a : β), a ∈ s₂ → f a = g a) :
s₁.sup f = s₂.sup g

source
@[simp]
theorem finset.sup_le_iff {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f : β → α} {a : α} :
s.sup f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a

source
theorem finset.sup_le {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f : β → α} {a : α} (a_1 : ∀ (b : β), b ∈ s → f b ≤ a) :
s.sup f ≤ a

source
theorem finset.le_sup {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f : β → α} {b : β} (hb : b ∈ s) :
f b ≤ s.sup f

source
theorem finset.sup_mono_fun {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f g : β → α} (h : ∀ (b : β), b ∈ s → f b ≤ g b) :
s.sup f ≤ s.sup g

source
theorem finset.sup_mono {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ ⊆ s₂) :
s₁.sup f ≤ s₂.sup f

source
@[simp]
theorem finset.sup_lt_iff {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f : β → α} [is_total α has_le.le] {a : α} (ha : ⊥ < a) :
s.sup f < a ↔ ∀ (b : β), b ∈ s → f b < a

source
theorem finset.comp_sup_eq_sup_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup_bot α] [semilattice_sup_bot γ] {s : finset β} {f : β → α} (g : α → γ) (g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) (bot : g ⊥ = ⊥) :
g (s.sup f) = s.sup (g ∘ f)

source
theorem finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {s : finset β} {f : β → α} [is_total α has_le.le] {γ : Type} [semilattice_sup_bot γ] (g : α → γ) (mono_g : monotone g) (bot : g ⊥ = ⊥) :
g (s.sup f) = s.sup (g ∘ f)

source
theorem finset.sup_coe {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] {P : α → Prop} {Pbot : P ⊥} {Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)} (t : finset β) (f : β → {x // P x}) :
↑(t.sup f) = t.sup (λ (x : β), ↑(f x))

Computating sup in a subtype (closed under sup) is the same as computing it in α.

source
theorem finset.subset_range_sup_succ (s : finset ℕ) :
s ⊆ finset.range (s.sup id).succ

source
theorem finset.exists_nat_subset_range (s : finset ℕ) :
∃ (n : ℕ), s ⊆ finset.range n

source
theorem finset.mem_sup {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α → multiset β} {x : β} :
x ∈ s.sup f ↔ ∃ (v : α) (H : v ∈ s), x ∈ f v

source
theorem finset.sup_subset {α : Type u_1} {β : Type u_2} [semilattice_sup_bot β] {s t : finset α} (hst : s ⊆ t) (f : α → β) :
s.sup f ≤ t.sup f

source
theorem finset.sup_eq_supr {α : Type u_1} {β : Type u_2} [complete_lattice β] (s : finset α) (f : α → β) :
s.sup f = ⨆ (a : α) (H : a ∈ s), f a

inf

source
def finset.inf {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] (s : finset β) (f : β → α) :
α

Infimum of a finite set: inf {a, b, c} f = f a ⊓ f b ⊓ f c

Equations
source
theorem finset.inf_def {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f : β → α} :
s.inf f = (multiset.map f s.val).inf

source
@[simp]
theorem finset.inf_empty {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {f : β → α} :
∅.inf f = ⊤

source
theorem finset.le_inf_iff {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f : β → α} {a : α} :
a ≤ s.inf f ↔ ∀ (b : β), b ∈ s → a ≤ f b

source
@[simp]
theorem finset.inf_insert {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).inf f = f b ⊓ s.inf f

source
@[simp]
theorem finset.inf_singleton {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {f : β → α} {b : β} :
{b}.inf f = f b

source
theorem finset.inf_union {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f

source
theorem finset.inf_congr {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (a : β), a ∈ s₂ → f a = g a) :
s₁.inf f = s₂.inf g

source
theorem finset.inf_le {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f : β → α} {b : β} (hb : b ∈ s) :
s.inf f ≤ f b

source
theorem finset.le_inf {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f : β → α} {a : α} (a_1 : ∀ (b : β), b ∈ s → a ≤ f b) :
a ≤ s.inf f

source
theorem finset.inf_mono_fun {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f g : β → α} (h : ∀ (b : β), b ∈ s → f b ≤ g b) :
s.inf f ≤ s.inf g

source
theorem finset.inf_mono {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ ⊆ s₂) :
s₂.inf f ≤ s₁.inf f

source
theorem finset.lt_inf_iff {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f : β → α} [h : is_total α has_le.le] {a : α} (ha : a < ⊤) :
a < s.inf f ↔ ∀ (b : β), b ∈ s → a < f b

source
theorem finset.comp_inf_eq_inf_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf_top α] [semilattice_inf_top γ] {s : finset β} {f : β → α} (g : α → γ) (g_inf : ∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) (top : g ⊤ = ⊤) :
g (s.inf f) = s.inf (g ∘ f)

source
theorem finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {s : finset β} {f : β → α} [h : is_total α has_le.le] {γ : Type} [semilattice_inf_top γ] (g : α → γ) (mono_g : monotone g) (top : g ⊤ = ⊤) :
g (s.inf f) = s.inf (g ∘ f)

source
theorem finset.inf_coe {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] {P : α → Prop} {Ptop : P ⊤} {Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)} (t : finset β) (f : β → {x // P x}) :
↑(t.inf f) = t.inf (λ (x : β), ↑(f x))

Computating inf in a subtype (closed under inf) is the same as computing it in α.

source
theorem finset.inf_eq_infi {α : Type u_1} {β : Type u_2} [complete_lattice β] (s : finset α) (f : α → β) :
s.inf f = ⨅ (a : α) (H : a ∈ s), f a

max and min of finite sets

source
def finset.max {α : Type u_1} [decidable_linear_order α] (a : finset α) :
option α

Let s be a finset in a linear order. Then s.max is the maximum of s if s is not empty, and none otherwise. It belongs to option α. If you want to get an element of α, see s.max'.

Equations
source
theorem finset.max_eq_sup_with_bot {α : Type u_1} [decidable_linear_order α] (s : finset α) :
s.max = s.sup some

source
@[simp]
theorem finset.max_empty {α : Type u_1} [decidable_linear_order α] :
∅.max = none

source
@[simp]
theorem finset.max_insert {α : Type u_1} [decidable_linear_order α] {a : α} {s : finset α} :
(insert a s).max = option.lift_or_get max (some a) s.max

source
@[simp]
theorem finset.max_singleton {α : Type u_1} [decidable_linear_order α] {a : α} :
{a}.max = some a

source
theorem finset.max_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a : α} (h : a ∈ s) :
∃ (b : α), b ∈ s.max

source
theorem finset.max_of_nonempty {α : Type u_1} [decidable_linear_order α] {s : finset α} (h : s.nonempty) :
∃ (a : α), a ∈ s.max

source
theorem finset.max_eq_none {α : Type u_1} [decidable_linear_order α] {s : finset α} :
s.max = none ↔ s = ∅

source
theorem finset.mem_of_max {α : Type u_1} [decidable_linear_order α] {s : finset α} {a : α} (a_1 : a ∈ s.max) :
a ∈ s

source
theorem finset.le_max_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a b : α} (h₁ : a ∈ s) (h₂ : b ∈ s.max) :
a ≤ b

source
def finset.min {α : Type u_1} [decidable_linear_order α] (a : finset α) :
option α

Let s be a finset in a linear order. Then s.min is the minimum of s if s is not empty, and none otherwise. It belongs to option α. If you want to get an element of α, see s.min'.

Equations
source
theorem finset.min_eq_inf_with_top {α : Type u_1} [decidable_linear_order α] (s : finset α) :
s.min = s.inf some

source
@[simp]
theorem finset.min_empty {α : Type u_1} [decidable_linear_order α] :
∅.min = none

source
@[simp]
theorem finset.min_insert {α : Type u_1} [decidable_linear_order α] {a : α} {s : finset α} :
(insert a s).min = option.lift_or_get min (some a) s.min

source
@[simp]
theorem finset.min_singleton {α : Type u_1} [decidable_linear_order α] {a : α} :
{a}.min = some a

source
theorem finset.min_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a : α} (h : a ∈ s) :
∃ (b : α), b ∈ s.min

source
theorem finset.min_of_nonempty {α : Type u_1} [decidable_linear_order α] {s : finset α} (h : s.nonempty) :
∃ (a : α), a ∈ s.min

source
theorem finset.min_eq_none {α : Type u_1} [decidable_linear_order α] {s : finset α} :
s.min = none ↔ s = ∅

source
theorem finset.mem_of_min {α : Type u_1} [decidable_linear_order α] {s : finset α} {a : α} (a_1 : a ∈ s.min) :
a ∈ s

source
theorem finset.min_le_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a b : α} (h₁ : b ∈ s) (h₂ : a ∈ s.min) :
a ≤ b

source
def finset.min' {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) :
α

Given a nonempty finset s in a linear order α, then s.min' h is its minimum, as an element of α, where h is a proof of nonemptiness. Without this assumption, use instead s.min, taking values in option α.

Equations
source
def finset.max' {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) :
α

Given a nonempty finset s in a linear order α, then s.max' h is its maximum, as an element of α, where h is a proof of nonemptiness. Without this assumption, use instead s.max, taking values in option α.

Equations
source
theorem finset.min'_mem {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) :
s.min' H ∈ s

source
theorem finset.min'_le {α : Type u_1} [decidable_linear_order α] (s : finset α) (x : α) (H2 : x ∈ s) :
s.min' _ ≤ x

source
theorem finset.le_min' {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) (x : α) (H2 : ∀ (y : α), y ∈ s → x ≤ y) :
x ≤ s.min' H

source
@[simp]
theorem finset.min'_singleton {α : Type u_1} [decidable_linear_order α] (a : α) :
{a}.min' _ = a

{a}.min' _ is a.

source
theorem finset.max'_mem {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) :
s.max' H ∈ s

source
theorem finset.le_max' {α : Type u_1} [decidable_linear_order α] (s : finset α) (x : α) (H2 : x ∈ s) :
x ≤ s.max' _

source
theorem finset.max'_le {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) (x : α) (H2 : ∀ (y : α), y ∈ s → y ≤ x) :
s.max' H ≤ x

source
@[simp]
theorem finset.max'_singleton {α : Type u_1} [decidable_linear_order α] (a : α) :
{a}.max' _ = a

{a}.max' _ is a.

source
theorem finset.min'_lt_max' {α : Type u_1} [decidable_linear_order α] (s : finset α) {i j : α} (H1 : i ∈ s) (H2 : j ∈ s) (H3 : i ≠ j) :
s.min' _ < s.max' _

source
theorem finset.min'_lt_max'_of_card {α : Type u_1} [decidable_linear_order α] (s : finset α) (h₂ : 1 < s.card) :
s.min' _ < s.max' _

If there's more than 1 element, the min' is less than the max'. An alternate version of min'_lt_max' which is sometimes more convenient.

source
theorem finset.exists_max_image {α : Type u_1} {β : Type u_2} [linear_order α] (s : finset β) (f : β → α) (h : s.nonempty) :
∃ (x : β) (H : x ∈ s), ∀ (x' : β), x' ∈ s → f x' ≤ f x

source
theorem finset.exists_min_image {α : Type u_1} {β : Type u_2} [linear_order α] (s : finset β) (f : β → α) (h : s.nonempty) :
∃ (x : β) (H : x ∈ s), ∀ (x' : β), x' ∈ s → f x ≤ f x'

source
theorem multiset.count_sup {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → multiset β) (b : β) :
multiset.count b (s.sup f) = s.sup (λ (a : α), multiset.count b (f a))

source
theorem supr_eq_supr_finset {α : Type u_1} {ι : Type u_4} [complete_lattice α] (s : ι → α) :
(⨆ (i : ι), s i) = ⨆ (t : finset ι) (i : ι) (H : i ∈ t), s i

Supremum of s i, i : ι, is equal to the supremum over t : finset ι of suprema ⨆ i ∈ t, s i. This version assumes ι is a Type*. See supr_eq_supr_finset' for a version that works for ι : Sort*.

source
theorem supr_eq_supr_finset' {α : Type u_1} {ι' : Sort u_5} [complete_lattice α] (s : ι' → α) :
(⨆ (i : ι'), s i) = ⨆ (t : finset (plift ι')) (i : plift ι') (H : i ∈ t), s i.down

Supremum of s i, i : ι, is equal to the supremum over t : finset ι of suprema ⨆ i ∈ t, s i. This version works for ι : Sort*. See supr_eq_supr_finset for a version that assumes ι : Type* but has no plifts.

source
theorem infi_eq_infi_finset {α : Type u_1} {ι : Type u_4} [complete_lattice α] (s : ι → α) :
(⨅ (i : ι), s i) = ⨅ (t : finset ι) (i : ι) (H : i ∈ t), s i

Infimum of s i, i : ι, is equal to the infimum over t : finset ι of infima ⨆ i ∈ t, s i. This version assumes ι is a Type*. See infi_eq_infi_finset' for a version that works for ι : Sort*.

source
theorem infi_eq_infi_finset' {α : Type u_1} {ι' : Sort u_5} [complete_lattice α] (s : ι' → α) :
(⨅ (i : ι'), s i) = ⨅ (t : finset (plift ι')) (i : plift ι') (H : i ∈ t), s i.down

Infimum of s i, i : ι, is equal to the infimum over t : finset ι of infima ⨆ i ∈ t, s i. This version works for ι : Sort*. See infi_eq_infi_finset for a version that assumes ι : Type* but has no plifts.

source
theorem set.Union_eq_Union_finset {α : Type u_1} {ι : Type u_4} (s : ι → set α) :
(⋃ (i : ι), s i) = ⋃ (t : finset ι) (i : ι) (H : i ∈ t), s i

Union of an indexed family of sets s : ι → set α is equal to the union of the unions of finite subfamilies. This version assumes ι : Type*. See also Union_eq_Union_finset' for a version that works for ι : Sort*.

source
theorem set.Union_eq_Union_finset' {α : Type u_1} {ι' : Sort u_5} (s : ι' → set α) :
(⋃ (i : ι'), s i) = ⋃ (t : finset (plift ι')) (i : plift ι') (H : i ∈ t), s i.down

Union of an indexed family of sets s : ι → set α is equal to the union of the unions of finite subfamilies. This version works for ι : Sort*. See also Union_eq_Union_finset for a version that assumes ι : Type* but avoids plifts in the right hand side.

source
theorem set.Inter_eq_Inter_finset {α : Type u_1} {ι : Type u_4} (s : ι → set α) :
(⋂ (i : ι), s i) = ⋂ (t : finset ι) (i : ι) (H : i ∈ t), s i

Intersection of an indexed family of sets s : ι → set α is equal to the intersection of the intersections of finite subfamilies. This version assumes ι : Type*. See also Inter_eq_Inter_finset' for a version that works for ι : Sort*.

source
theorem set.Inter_eq_Inter_finset' {α : Type u_1} {ι' : Sort u_5} (s : ι' → set α) :
(⋂ (i : ι'), s i) = ⋂ (t : finset (plift ι')) (i : plift ι') (H : i ∈ t), s i.down

Intersection of an indexed family of sets s : ι → set α is equal to the intersection of the intersections of finite subfamilies. This version works for ι : Sort*. See also Inter_eq_Inter_finset for a version that assumes ι : Type* but avoids plifts in the right hand side.

Interaction with big lattice/set operations

source
theorem finset.supr_coe {α : Type u_1} {β : Type u_2} [has_Sup β] (f : α → β) (s : finset α) :
(⨆ (x : α) (H : x ∈ ↑s), f x) = ⨆ (x : α) (H : x ∈ s), f x

source
theorem finset.infi_coe {α : Type u_1} {β : Type u_2} [has_Inf β] (f : α → β) (s : finset α) :
(⨅ (x : α) (H : x ∈ ↑s), f x) = ⨅ (x : α) (H : x ∈ s), f x

source
theorem finset.supr_singleton {α : Type u_1} {β : Type u_2} [complete_lattice β] (a : α) (s : α → β) :
(⨆ (x : α) (H : x ∈ {a}), s x) = s a

source
theorem finset.infi_singleton {α : Type u_1} {β : Type u_2} [complete_lattice β] (a : α) (s : α → β) :
(⨅ (x : α) (H : x ∈ {a}), s x) = s a

source
theorem finset.supr_option_to_finset {α : Type u_1} {β : Type u_2} [complete_lattice β] (o : option α) (f : α → β) :
(⨆ (x : α) (H : x ∈ o.to_finset), f x) = ⨆ (x : α) (H : x ∈ o), f x

source
theorem finset.infi_option_to_finset {α : Type u_1} {β : Type u_2} [complete_lattice β] (o : option α) (f : α → β) :
(⨅ (x : α) (H : x ∈ o.to_finset), f x) = ⨅ (x : α) (H : x ∈ o), f x

source
theorem finset.supr_union {α : Type u_1} {β : Type u_2} [complete_lattice β] [decidable_eq α] {f : α → β} {s t : finset α} :
(⨆ (x : α) (H : x ∈ s ∪ t), f x) = (⨆ (x : α) (H : x ∈ s), f x) ⊔ ⨆ (x : α) (H : x ∈ t), f x

source
theorem finset.infi_union {α : Type u_1} {β : Type u_2} [complete_lattice β] [decidable_eq α] {f : α → β} {s t : finset α} :
(⨅ (x : α) (H : x ∈ s ∪ t), f x) = (⨅ (x : α) (H : x ∈ s), f x) ⊓ ⨅ (x : α) (H : x ∈ t), f x

source
theorem finset.supr_insert {α : Type u_1} {β : Type u_2} [complete_lattice β] [decidable_eq α] (a : α) (s : finset α) (t : α → β) :
(⨆ (x : α) (H : x ∈ insert a s), t x) = t a ⊔ ⨆ (x : α) (H : x ∈ s), t x

source
theorem finset.infi_insert {α : Type u_1} {β : Type u_2} [complete_lattice β] [decidable_eq α] (a : α) (s : finset α) (t : α → β) :
(⨅ (x : α) (H : x ∈ insert a s), t x) = t a ⊓ ⨅ (x : α) (H : x ∈ s), t x

source
theorem finset.supr_finset_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [complete_lattice β] [decidable_eq α] {f : γ → α} {g : α → β} {s : finset γ} :
(⨆ (x : α) (H : x ∈ finset.image f s), g x) = ⨆ (y : γ) (H : y ∈ s), g (f y)

source
theorem finset.infi_finset_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [complete_lattice β] [decidable_eq α] {f : γ → α} {g : α → β} {s : finset γ} :
(⨅ (x : α) (H : x ∈ finset.image f s), g x) = ⨅ (y : γ) (H : y ∈ s), g (f y)

source
theorem finset.supr_insert_update {α : Type u_1} {β : Type u_2} [complete_lattice β] [decidable_eq α] {x : α} {t : finset α} (f : α → β) {s : β} (hx : x ∉ t) :
(⨆ (i : α) (H : i ∈ insert x t), function.update f x s i) = s ⊔ ⨆ (i : α) (H : i ∈ t), f i

source
theorem finset.infi_insert_update {α : Type u_1} {β : Type u_2} [complete_lattice β] [decidable_eq α] {x : α} {t : finset α} (f : α → β) {s : β} (hx : x ∉ t) :
(⨅ (i : α) (H : i ∈ insert x t), function.update f x s i) = s ⊓ ⨅ (i : α) (H : i ∈ t), f i

source
theorem finset.supr_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [complete_lattice β] [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → β) :
(⨆ (y : α) (H : y ∈ s.bind t), f y) = ⨆ (x : γ) (H : x ∈ s) (y : α) (H : y ∈ t x), f y

source
theorem finset.infi_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [complete_lattice β] [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → β) :
(⨅ (y : α) (H : y ∈ s.bind t), f y) = ⨅ (x : γ) (H : x ∈ s) (y : α) (H : y ∈ t x), f y

source
@[simp]
theorem finset.bUnion_coe {α : Type u_1} {β : Type u_2} (s : finset α) (t : α → set β) :
(⋃ (x : α) (H : x ∈ ↑s), t x) = ⋃ (x : α) (H : x ∈ s), t x

source
@[simp]
theorem finset.bInter_coe {α : Type u_1} {β : Type u_2} (s : finset α) (t : α → set β) :
(⋂ (x : α) (H : x ∈ ↑s), t x) = ⋂ (x : α) (H : x ∈ s), t x

source
@[simp]
theorem finset.bUnion_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → set β) :
(⋃ (x : α) (H : x ∈ {a}), s x) = s a

source
@[simp]
theorem finset.bInter_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → set β) :
(⋂ (x : α) (H : x ∈ {a}), s x) = s a

source
@[simp]
theorem finset.bUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (s : finset β) :
(⋃ (y : β) (H : y ∈ s), f ⁻¹' {y}) = f ⁻¹' ↑s

source
@[simp]
theorem finset.bUnion_option_to_finset {α : Type u_1} {β : Type u_2} (o : option α) (f : α → set β) :
(⋃ (x : α) (H : x ∈ o.to_finset), f x) = ⋃ (x : α) (H : x ∈ o), f x

source
@[simp]
theorem finset.bInter_option_to_finset {α : Type u_1} {β : Type u_2} (o : option α) (f : α → set β) :
(⋂ (x : α) (H : x ∈ o.to_finset), f x) = ⋂ (x : α) (H : x ∈ o), f x

source
theorem finset.bUnion_union {α : Type u_1} {β : Type u_2} [decidable_eq α] (s t : finset α) (u : α → set β) :
(⋃ (x : α) (H : x ∈ s ∪ t), u x) = (⋃ (x : α) (H : x ∈ s), u x) ∪ ⋃ (x : α) (H : x ∈ t), u x

source
theorem finset.bInter_inter {α : Type u_1} {β : Type u_2} [decidable_eq α] (s t : finset α) (u : α → set β) :
(⋂ (x : α) (H : x ∈ s ∪ t), u x) = (⋂ (x : α) (H : x ∈ s), u x) ∩ ⋂ (x : α) (H : x ∈ t), u x

source
@[simp]
theorem finset.bUnion_insert {α : Type u_1} {β : Type u_2} [decidable_eq α] (a : α) (s : finset α) (t : α → set β) :
(⋃ (x : α) (H : x ∈ insert a s), t x) = t a ∪ ⋃ (x : α) (H : x ∈ s), t x

source
@[simp]
theorem finset.bInter_insert {α : Type u_1} {β : Type u_2} [decidable_eq α] (a : α) (s : finset α) (t : α → set β) :
(⋂ (x : α) (H : x ∈ insert a s), t x) = t a ∩ ⋂ (x : α) (H : x ∈ s), t x

source
@[simp]
theorem finset.bUnion_finset_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] {f : γ → α} {g : α → set β} {s : finset γ} :
(⋃ (x : α) (H : x ∈ finset.image f s), g x) = ⋃ (y : γ) (H : y ∈ s), g (f y)

source
@[simp]
theorem finset.bInter_finset_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] {f : γ → α} {g : α → set β} {s : finset γ} :
(⋂ (x : α) (H : x ∈ finset.image f s), g x) = ⋂ (y : γ) (H : y ∈ s), g (f y)

source
theorem finset.bUnion_insert_update {α : Type u_1} {β : Type u_2} [decidable_eq α] {x : α} {t : finset α} (f : α → set β) {s : set β} (hx : x ∉ t) :
(⋃ (i : α) (H : i ∈ insert x t), function.update f x s i) = s ∪ ⋃ (i : α) (H : i ∈ t), f i

source
theorem finset.bInter_insert_update {α : Type u_1} {β : Type u_2} [decidable_eq α] {x : α} {t : finset α} (f : α → set β) {s : set β} (hx : x ∉ t) :
(⋂ (i : α) (H : i ∈ insert x t), function.update f x s i) = s ∩ ⋂ (i : α) (H : i ∈ t), f i

source
@[simp]
theorem finset.bUnion_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → set β) :
(⋃ (y : α) (H : y ∈ s.bind t), f y) = ⋃ (x : γ) (H : x ∈ s) (y : α) (H : y ∈ t x), f y

source
@[simp]
theorem finset.bInter_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → set β) :
(⋂ (y : α) (H : y ∈ s.bind t), f y) = ⋂ (x : γ) (H : x ∈ s) (y : α) (H : y ∈ t x), f y