# mathlibdocumentation

data.finset.lattice

# Lattice operations on finsets

### sup

def finset.sup {α : Type u_1} {β : Type u_2}  :
(β → α) → α

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

Equations
theorem finset.sup_def {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} :
s.sup f = s.val).sup

@[simp]
theorem finset.sup_empty {α : Type u_1} {β : Type u_2} {f : β → α} :

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

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

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

theorem finset.sup_congr {α : Type u_1} {β : Type u_2} {s₁ s₂ : finset β} {f g : β → α} :
s₁ = s₂(∀ (a : β), a s₂f a = g a)s₁.sup f = s₂.sup g

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

theorem finset.sup_le {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sf b a)s.sup f a

theorem finset.le_sup {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} {b : β} :
b sf b s.sup f

theorem finset.sup_mono_fun {α : Type u_1} {β : Type u_2} {s : finset β} {f g : β → α} :
(∀ (b : β), b sf b g b)s.sup f s.sup g

theorem finset.sup_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : finset β} {f : β → α} :
s₁ s₂s₁.sup f s₂.sup f

@[simp]
theorem finset.sup_lt_iff {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} {a : α} :
< a(s.sup f < a ∀ (b : β), b sf b < a)

theorem finset.comp_sup_eq_sup_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : finset β} {f : β → α} (g : α → γ) :
(∀ (x y : α), g (x y) = g x g y)g = g (s.sup f) = s.sup (g f)

theorem finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} {γ : Type} (g : α → γ) :
g = g (s.sup f) = s.sup (g f)

theorem finset.sup_coe {α : Type u_1} {β : Type u_2} {P : α → Prop} {Pbot : P } {Psup : ∀ ⦃x y : α⦄, P xP yP (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 α.

theorem finset.exists_nat_subset_range (s : finset ) :
∃ (n : ),

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

theorem finset.sup_subset {α : Type u_1} {β : Type u_2} {s t : finset α} (hst : s t) (f : α → β) :
s.sup f t.sup f

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

### inf

def finset.inf {α : Type u_1} {β : Type u_2}  :
(β → α) → α

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

Equations
theorem finset.inf_def {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} :
s.inf f = s.val).inf

@[simp]
theorem finset.inf_empty {α : Type u_1} {β : Type u_2} {f : β → α} :

theorem finset.le_inf_iff {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} {a : α} :
a s.inf f ∀ (b : β), b sa f b

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

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

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

theorem finset.inf_congr {α : Type u_1} {β : Type u_2} {s₁ s₂ : finset β} {f g : β → α} :
s₁ = s₂(∀ (a : β), a s₂f a = g a)s₁.inf f = s₂.inf g

theorem finset.inf_le {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} {b : β} :
b ss.inf f f b

theorem finset.le_inf {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sa f b)a s.inf f

theorem finset.inf_mono_fun {α : Type u_1} {β : Type u_2} {s : finset β} {f g : β → α} :
(∀ (b : β), b sf b g b)s.inf f s.inf g

theorem finset.inf_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : finset β} {f : β → α} :
s₁ s₂s₂.inf f s₁.inf f

theorem finset.lt_inf_iff {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} [h : has_le.le] {a : α} :
a < (a < s.inf f ∀ (b : β), b sa < f b)

theorem finset.comp_inf_eq_inf_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : finset β} {f : β → α} (g : α → γ) :
(∀ (x y : α), g (x y) = g x g y)g = g (s.inf f) = s.inf (g f)

theorem finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_1} {β : Type u_2} {s : finset β} {f : β → α} [h : has_le.le] {γ : Type} (g : α → γ) :
g = g (s.inf f) = s.inf (g f)

theorem finset.inf_coe {α : Type u_1} {β : Type u_2} {P : α → Prop} {Ptop : P } {Pinf : ∀ ⦃x y : α⦄, P xP yP (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 α.

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

### max and min of finite sets

def finset.max {α : Type u_1} [linear_order α] :

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
theorem finset.max_eq_sup_with_bot {α : Type u_1} [linear_order α] (s : finset α) :

@[simp]
theorem finset.max_empty {α : Type u_1} [linear_order α] :

@[simp]
theorem finset.max_insert {α : Type u_1} [linear_order α] {a : α} {s : finset α} :
(insert a s).max = s.max

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

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

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

theorem finset.max_eq_none {α : Type u_1} [linear_order α] {s : finset α} :

theorem finset.mem_of_max {α : Type u_1} [linear_order α] {s : finset α} {a : α} :
a s.maxa s

theorem finset.le_max_of_mem {α : Type u_1} [linear_order α] {s : finset α} {a b : α} :
a sb s.maxa b

def finset.min {α : Type u_1} [linear_order α] :

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
theorem finset.min_eq_inf_with_top {α : Type u_1} [linear_order α] (s : finset α) :

@[simp]
theorem finset.min_empty {α : Type u_1} [linear_order α] :

@[simp]
theorem finset.min_insert {α : Type u_1} [linear_order α] {a : α} {s : finset α} :
(insert a s).min = s.min

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

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

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

theorem finset.min_eq_none {α : Type u_1} [linear_order α] {s : finset α} :

theorem finset.mem_of_min {α : Type u_1} [linear_order α] {s : finset α} {a : α} :
a s.mina s

theorem finset.min_le_of_mem {α : Type u_1} [linear_order α] {s : finset α} {a b : α} :
b sa s.mina b

def finset.min' {α : Type u_1} [linear_order α] (s : finset α) :
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
def finset.max' {α : Type u_1} [linear_order α] (s : finset α) :
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
theorem finset.min'_mem {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) :
s.min' H s

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

theorem finset.le_min' {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) (x : α) :
(∀ (y : α), y sx y)x s.min' H

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

{a}.min' _ is a.

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

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

theorem finset.max'_le {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) (x : α) :
(∀ (y : α), y sy x)s.max' H x

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

{a}.max' _ is a.

theorem finset.min'_lt_max' {α : Type u_1} [linear_order α] (s : finset α) {i j : α} (H1 : i s) :
j si js.min' _ < s.max' _

theorem finset.min'_lt_max'_of_card {α : Type u_1} [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.

theorem finset.max'_eq_of_dual_min' {α : Type u_1} [linear_order α] {s : finset α} (hs : s.nonempty) :
s.max' hs =

theorem finset.min'_eq_of_dual_max' {α : Type u_1} [linear_order α] {s : finset α} (hs : s.nonempty) :
s.min' hs =

@[simp]
theorem finset.of_dual_max_eq_min_of_dual {α : Type u_1} [linear_order α] {a b : α} :

@[simp]
theorem finset.of_dual_min_eq_max_of_dual {α : Type u_1} [linear_order α] {a b : α} :

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

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

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

theorem supr_eq_supr_finset {α : Type u_1} {ι : Type u_4} (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*.

theorem supr_eq_supr_finset' {α : Type u_1} {ι' : Sort u_5} (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.

theorem infi_eq_infi_finset {α : Type u_1} {ι : Type u_4} (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*.

theorem infi_eq_infi_finset' {α : Type u_1} {ι' : Sort u_5} (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.

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*.

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.

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*.

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

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

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

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

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

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

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

theorem finset.supr_union {α : Type u_1} {β : Type u_2} [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

theorem finset.infi_union {α : Type u_1} {β : Type u_2} [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

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

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

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

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

theorem finset.supr_insert_update {α : Type u_1} {β : Type u_2} [decidable_eq α] {x : α} {t : finset α} (f : α → β) {s : β} :
x t((⨆ (i : α) (H : i t), s i) = s ⨆ (i : α) (H : i t), f i)

theorem finset.infi_insert_update {α : Type u_1} {β : Type u_2} [decidable_eq α] {x : α} {t : finset α} (f : α → β) {s : β} :
x t((⨅ (i : α) (H : i t), s i) = s ⨅ (i : α) (H : i t), f i)

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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 s), g x) = ⋃ (y : γ) (H : y s), g (f y)

@[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 s), g x) = ⋂ (y : γ) (H : y s), g (f y)

theorem finset.bUnion_insert_update {α : Type u_1} {β : Type u_2} [decidable_eq α] {x : α} {t : finset α} (f : α → set β) {s : set β} :
x t((⋃ (i : α) (H : i t), s i) = s ⋃ (i : α) (H : i t), f i)

theorem finset.bInter_insert_update {α : Type u_1} {β : Type u_2} [decidable_eq α] {x : α} {t : finset α} (f : α → set β) {s : set β} :
x t((⋂ (i : α) (H : i t), s i) = s ⋂ (i : α) (H : i t), f i)

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

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