mathlib docs: data.finset.lattice

source

def finset.sup {α : Type u_1} {β : Type u_2} [semilattice_sup_bot α] :

finset β → (β → α) → α

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

Equations

s.sup f = finset.fold has_sup.sup ⊥ f s

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 : β} :

(has_insert.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 : β → α} :

s₁ = s₂ → (∀ (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 : α} :

(∀ (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 : β} :

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 : β → α} :

(∀ (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 : β → α} :

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 : α} :

⊥ < 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 : α → γ) :

(∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → 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 : α → γ) :

monotone g → 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.sup_eq_supr {α : Type u_1} {β : Type u_2} [complete_lattice β] (s : finset α) (f : α → β) :

s.sup f = ⨆ (a : α) (H : a ∈ s), f a

source

def finset.inf {α : Type u_1} {β : Type u_2} [semilattice_inf_top α] :

finset β → (β → α) → α

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

Equations

s.inf f = finset.fold has_inf.inf ⊤ f s

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 : β} :

(has_insert.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 : β → α} :

s₁ = s₂ → (∀ (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 : β} :

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 : α} :

(∀ (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 : β → α} :

(∀ (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 : β → α} :

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 : α} :

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 : α → γ) :

(∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) → 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 : α → γ) :

monotone g → 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

source

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

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

finset.max = finset.fold (option.lift_or_get max) option.none option.some

source

theorem finset.max_eq_sup_with_bot {α : Type u_1} [decidable_linear_order α] (s : finset α) :

s.max = s.sup option.some

source

@[simp]

theorem finset.max_empty {α : Type u_1} [decidable_linear_order α] :

∅.max = option.none

source

@[simp]

theorem finset.max_insert {α : Type u_1} [decidable_linear_order α] {a : α} {s : finset α} :

(has_insert.insert a s).max = option.lift_or_get max (option.some a) s.max

source

@[simp]

theorem finset.max_singleton {α : Type u_1} [decidable_linear_order α] {a : α} :

{a}.max = option.some a

source

theorem finset.max_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a : α} :

a ∈ s → (∃ (b : α), b ∈ s.max)

source

theorem finset.max_of_nonempty {α : Type u_1} [decidable_linear_order α] {s : finset α} :

s.nonempty → (∃ (a : α), a ∈ s.max)

source

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

s.max = option.none ↔ s = ∅

source

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

a ∈ s.max → a ∈ s

source

theorem finset.le_max_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a b : α} :

a ∈ s → b ∈ s.max → a ≤ b

source

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

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

finset.min = finset.fold (option.lift_or_get min) option.none option.some

source

theorem finset.min_eq_inf_with_top {α : Type u_1} [decidable_linear_order α] (s : finset α) :

s.min = s.inf option.some

source

@[simp]

theorem finset.min_empty {α : Type u_1} [decidable_linear_order α] :

∅.min = option.none

source

@[simp]

theorem finset.min_insert {α : Type u_1} [decidable_linear_order α] {a : α} {s : finset α} :

(has_insert.insert a s).min = option.lift_or_get min (option.some a) s.min

source

@[simp]

theorem finset.min_singleton {α : Type u_1} [decidable_linear_order α] {a : α} :

{a}.min = option.some a

source

theorem finset.min_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a : α} :

a ∈ s → (∃ (b : α), b ∈ s.min)

source

theorem finset.min_of_nonempty {α : Type u_1} [decidable_linear_order α] {s : finset α} :

s.nonempty → (∃ (a : α), a ∈ s.min)

source

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

s.min = option.none ↔ s = ∅

source

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

a ∈ s.min → a ∈ s

source

theorem finset.min_le_of_mem {α : Type u_1} [decidable_linear_order α] {s : finset α} {a b : α} :

b ∈ s → a ∈ s.min → a ≤ b

source

def finset.min' {α : Type u_1} [decidable_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

s.min' H = option.get _
_ = _
_ = _

source

def finset.max' {α : Type u_1} [decidable_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

s.max' H = option.get _
_ = _
_ = _

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 α) (H : s.nonempty) (x : α) :

x ∈ s → s.min' H ≤ x

source

theorem finset.le_min' {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) (x : α) :

(∀ (y : α), y ∈ s → x ≤ y) → x ≤ s.min' H

source

@[simp]

theorem finset.min'_singleton {α : Type u_1} [decidable_linear_order α] (a : α) {h : {a}.nonempty} :

{a}.min' h = 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 α) (H : s.nonempty) (x : α) :

x ∈ s → x ≤ s.max' H

source

theorem finset.max'_le {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) (x : α) :

(∀ (y : α), y ∈ s → y ≤ x) → s.max' H ≤ x

source

@[simp]

theorem finset.max'_singleton {α : Type u_1} [decidable_linear_order α] (a : α) {h : {a}.nonempty} :

{a}.max' h = a

{a}.max' is a.

source

theorem finset.min'_lt_max' {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) {i j : α} :

i ∈ s → j ∈ s → i ≠ j → s.min' H < s.max' H

source

theorem finset.min'_lt_max'_of_card {α : Type u_1} [decidable_linear_order α] (s : finset α) (H : s.nonempty) :

1 < s.card → s.min' H < s.max' H

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 : β → α) :

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 : β → α) :

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.

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_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 ∈ has_insert.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 ∈ has_insert.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 : β} :

x ∉ t → ((⨆ (i : α) (H : i ∈ has_insert.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 : β} :

x ∉ t → ((⨅ (i : α) (H : i ∈ has_insert.insert x t), function.update f x s i) = s ⊓ ⨅ (i : α) (H : i ∈ t), f i)

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

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 ∈ has_insert.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 ∈ has_insert.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 β} :

x ∉ t → ((⋃ (i : α) (H : i ∈ has_insert.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 β} :

x ∉ t → ((⋂ (i : α) (H : i ∈ has_insert.insert x t), function.update f x s i) = s ∩ ⋂ (i : α) (H : i ∈ t), f i)

mathlib documentation

data.finset.lattice

Lattice operations on multisets

sup

inf

max and min of finite sets

Interaction with big lattice/set operations

General documentation

Additional documentation

Library

mathlib documentation

data.​finset.​lattice

Lattice operations on multisets

sup

inf

max and min of finite sets

Interaction with big lattice/set operations

General documentation

Additional documentation

Library

data.finset.lattice