mathlib documentation

data.finset.lattice

Lattice operations on finsets #

sup #

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

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} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} :
@[simp]
theorem finset.sup_empty {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {f : β → α} :
@[simp]
theorem finset.sup_cons {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} {b : β} (h : b s) :
(finset.cons b s h).sup f = f b s.sup f
@[simp]
theorem finset.sup_insert {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).sup f = f b s.sup f
theorem finset.sup_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [order_bot α] [decidable_eq β] (s : finset γ) (f : γ → β) (g : β → α) :
(finset.image f s).sup g = s.sup (g f)
@[simp]
theorem finset.sup_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [order_bot α] (s : finset γ) (f : γ β) (g : β → α) :
(finset.map f s).sup g = s.sup (g f)
@[simp]
theorem finset.sup_singleton {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {f : β → α} {b : β} :
{b}.sup f = f b
theorem finset.sup_union {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ s₂).sup f = s₁.sup f s₂.sup f
theorem finset.sup_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f g : β → α} :
s.sup (f g) = s.sup f s.sup g
theorem finset.sup_congr {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (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} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} {a : α} :
s.sup f a ∀ (b : β), b sf b a
@[simp]
theorem finset.sup_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [order_bot α] {f : β → α} [decidable_eq β] (s : finset γ) (t : γ → finset β) :
(s.bUnion t).sup f = s.sup (λ (x : γ), (t x).sup f)
theorem finset.sup_const {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} (h : s.nonempty) (c : α) :
s.sup (λ (_x : β), c) = c
@[simp]
theorem finset.sup_bot {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] (s : finset β) :
s.sup (λ (_x : β), ) =
theorem finset.sup_ite {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f g : β → α} (p : β → Prop) [decidable_pred p] :
s.sup (λ (i : β), ite (p i) (f i) (g i)) = (finset.filter p s).sup f (finset.filter (λ (i : β), ¬p i) s).sup g
theorem finset.sup_le {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sf b a)s.sup f a
theorem finset.le_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} {b : β} (hb : b s) :
f b s.sup f
theorem finset.sup_mono_fun {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f g : β → α} (h : ∀ (b : β), b sf b g b) :
s.sup f s.sup g
theorem finset.sup_mono {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ s₂) :
s₁.sup f s₂.sup f
@[simp]
theorem finset.sup_lt_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} [is_total α has_le.le] {a : α} (ha : < a) :
s.sup f < a ∀ (b : β), b sf b < a
@[simp]
theorem finset.le_sup_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} [is_total α has_le.le] {a : α} (ha : < a) :
a s.sup f ∃ (b : β) (H : b s), a f b
@[simp]
theorem finset.lt_sup_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} [is_total α has_le.le] {a : α} :
a < s.sup f ∃ (b : β) (H : b s), a < f b
theorem finset.sup_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [order_bot α] (s : finset β) (t : finset γ) (f : β → γ → α) :
s.sup (λ (b : β), t.sup (f b)) = t.sup (λ (c : γ), s.sup (λ (b : β), f b c))
@[simp]
theorem finset.sup_attach {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] (s : finset β) (f : β → α) :
s.attach.sup (λ (x : {x // x s}), f x) = s.sup f
theorem finset.sup_product_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [order_bot α] (s : finset β) (t : finset γ) (f : β × γ → α) :
(s.product t).sup f = s.sup (λ (i : β), t.sup (λ (i' : γ), f (i, i')))

See also finset.product_bUnion.

theorem finset.sup_product_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [order_bot α] (s : finset β) (t : finset γ) (f : β × γ → α) :
(s.product t).sup f = t.sup (λ (i' : γ), s.sup (λ (i : β), f (i, i')))
@[simp]
theorem finset.sup_erase_bot {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (s : finset α) :
theorem finset.sup_sdiff_right {α : Type u_1} {β : Type u_2} [generalized_boolean_algebra α] (s : finset β) (f : β → α) (a : α) :
s.sup (λ (b : β), f b \ a) = s.sup f \ a
theorem finset.comp_sup_eq_sup_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [order_bot α] [semilattice_sup γ] [order_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)
theorem finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} [is_total α has_le.le] {γ : Type} [semilattice_sup γ] [order_bot γ] (g : α → γ) (mono_g : monotone g) (bot : g = ) :
g (s.sup f) = s.sup (g f)
theorem finset.sup_coe {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {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))

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

@[simp]
theorem finset.sup_to_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → multiset β) :
(s.sup f).to_finset = s.sup (λ (x : α), (f x).to_finset)
theorem finset.sup_induction {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} {f : β → α} {p : α → Prop} (hb : p ) (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : ∀ (b : β), b sp (f b)) :
p (s.sup f)
theorem finset.sup_le_of_le_directed {α : Type u_1} [semilattice_sup α] [order_bot α] (s : set α) (hs : s.nonempty) (hdir : directed_on has_le.le s) (t : finset α) :
(∀ (x : α), x t(∃ (y : α) (H : y s), x y))(∃ (x : α), x s t.sup id x)
theorem finset.sup_mem {α : Type u_1} [semilattice_sup α] [order_bot α] (s : set α) (w₁ : s) (w₂ : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : finset ι) (p : ι → α) (h : ∀ (i : ι), i tp i s) :
t.sup p s
@[simp]
theorem finset.sup_eq_bot_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] (f : β → α) (S : finset β) :
S.sup f = ∀ (s : β), s Sf s =
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
theorem finset.sup_id_eq_Sup {α : Type u_1} [complete_lattice α] (s : finset α) :
theorem finset.sup_id_set_eq_sUnion {α : Type u_1} (s : finset (set α)) :
@[simp]
theorem finset.sup_set_eq_bUnion {α : Type u_1} {β : Type u_2} (s : finset α) (f : α → set β) :
s.sup f = ⋃ (x : α) (H : x s), f x
theorem finset.sup_eq_Sup_image {α : Type u_1} {β : Type u_2} [complete_lattice β] (s : finset α) (f : α → β) :
s.sup f = Sup (f '' s)

inf #

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

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} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} :
@[simp]
theorem finset.inf_empty {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {f : β → α} :
@[simp]
theorem finset.inf_cons {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} {b : β} (h : b s) :
(finset.cons b s h).inf f = f b s.inf f
@[simp]
theorem finset.inf_insert {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).inf f = f b s.inf f
theorem finset.inf_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [order_top α] [decidable_eq β] (s : finset γ) (f : γ → β) (g : β → α) :
(finset.image f s).inf g = s.inf (g f)
@[simp]
theorem finset.inf_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [order_top α] (s : finset γ) (f : γ β) (g : β → α) :
(finset.map f s).inf g = s.inf (g f)
@[simp]
theorem finset.inf_singleton {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {f : β → α} {b : β} :
{b}.inf f = f b
theorem finset.inf_union {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ s₂).inf f = s₁.inf f s₂.inf f
theorem finset.inf_inf {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f g : β → α} :
s.inf (f g) = s.inf f s.inf g
theorem finset.inf_congr {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (a : β), a s₂f a = g a) :
s₁.inf f = s₂.inf g
@[simp]
theorem finset.inf_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [order_top α] {f : β → α} [decidable_eq β] (s : finset γ) (t : γ → finset β) :
(s.bUnion t).inf f = s.inf (λ (x : γ), (t x).inf f)
theorem finset.inf_const {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} (h : s.nonempty) (c : α) :
s.inf (λ (_x : β), c) = c
@[simp]
theorem finset.inf_top {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] (s : finset β) :
s.inf (λ (_x : β), ) =
theorem finset.le_inf_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} {a : α} :
a s.inf f ∀ (b : β), b sa f b
theorem finset.inf_le {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} {b : β} (hb : b s) :
s.inf f f b
theorem finset.le_inf {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sa f b)a s.inf f
theorem finset.inf_mono_fun {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f g : β → α} (h : ∀ (b : β), b sf b g b) :
s.inf f s.inf g
theorem finset.inf_mono {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ s₂) :
s₂.inf f s₁.inf f
@[simp]
theorem finset.lt_inf_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} [is_total α has_le.le] {a : α} (ha : a < ) :
a < s.inf f ∀ (b : β), b sa < f b
@[simp]
theorem finset.inf_le_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} [is_total α has_le.le] {a : α} (ha : a < ) :
s.inf f a ∃ (b : β) (H : b s), f b a
@[simp]
theorem finset.inf_lt_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} [is_total α has_le.le] {a : α} :
s.inf f < a ∃ (b : β) (H : b s), f b < a
theorem finset.inf_attach {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] (s : finset β) (f : β → α) :
s.attach.inf (λ (x : {x // x s}), f x) = s.inf f
theorem finset.inf_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [order_top α] (s : finset β) (t : finset γ) (f : β → γ → α) :
s.inf (λ (b : β), t.inf (f b)) = t.inf (λ (c : γ), s.inf (λ (b : β), f b c))
theorem finset.inf_product_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [order_top α] (s : finset β) (t : finset γ) (f : β × γ → α) :
(s.product t).inf f = s.inf (λ (i : β), t.inf (λ (i' : γ), f (i, i')))
theorem finset.inf_product_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [order_top α] (s : finset β) (t : finset γ) (f : β × γ → α) :
(s.product t).inf f = t.inf (λ (i' : γ), s.inf (λ (i : β), f (i, i')))
@[simp]
theorem finset.inf_erase_top {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (s : finset α) :
theorem finset.sup_sdiff_left {α : Type u_1} {β : Type u_2} [boolean_algebra α] (s : finset β) (f : β → α) (a : α) :
s.sup (λ (b : β), a \ f b) = a \ s.inf f
theorem finset.inf_sdiff_left {α : Type u_1} {β : Type u_2} [boolean_algebra α] {s : finset β} (hs : s.nonempty) (f : β → α) (a : α) :
s.inf (λ (b : β), a \ f b) = a \ s.sup f
theorem finset.inf_sdiff_right {α : Type u_1} {β : Type u_2} [boolean_algebra α] {s : finset β} (hs : s.nonempty) (f : β → α) (a : α) :
s.inf (λ (b : β), f b \ a) = s.inf f \ a
theorem finset.comp_inf_eq_inf_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [order_top α] [semilattice_inf γ] [order_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)
theorem finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} [h : is_total α has_le.le] {γ : Type} [semilattice_inf γ] [order_top γ] (g : α → γ) (mono_g : monotone g) (top : g = ) :
g (s.inf f) = s.inf (g f)
theorem finset.inf_coe {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {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))

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

theorem finset.inf_induction {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} {f : β → α} {p : α → Prop} (ht : p ) (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : ∀ (b : β), b sp (f b)) :
p (s.inf f)
theorem finset.inf_mem {α : Type u_1} [semilattice_inf α] [order_top α] (s : set α) (w₁ : s) (w₂ : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : finset ι) (p : ι → α) (h : ∀ (i : ι), i tp i s) :
t.inf p s
@[simp]
theorem finset.inf_eq_top_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] (f : β → α) (S : finset β) :
S.inf f = ∀ (s : β), s Sf s =
theorem finset.sup_inf_distrib_left {α : Type u_1} {ι : Type u_4} [distrib_lattice α] [order_bot α] (s : finset ι) (f : ι → α) (a : α) :
a s.sup f = s.sup (λ (i : ι), a f i)
theorem finset.sup_inf_distrib_right {α : Type u_1} {ι : Type u_4} [distrib_lattice α] [order_bot α] (s : finset ι) (f : ι → α) (a : α) :
s.sup f a = s.sup (λ (i : ι), f i a)
theorem finset.disjoint_sup_right {α : Type u_1} {β : Type u_2} [distrib_lattice α] [order_bot α] {s : finset β} {f : β → α} {a : α} :
disjoint a (s.sup f) ∀ (i : β), i sdisjoint a (f i)
theorem finset.disjoint_sup_left {α : Type u_1} {β : Type u_2} [distrib_lattice α] [order_bot α] {s : finset β} {f : β → α} {a : α} :
disjoint (s.sup f) a ∀ (i : β), i sdisjoint (f i) a
theorem finset.inf_sup_distrib_left {α : Type u_1} {ι : Type u_4} [distrib_lattice α] [order_top α] (s : finset ι) (f : ι → α) (a : α) :
a s.inf f = s.inf (λ (i : ι), a f i)
theorem finset.inf_sup_distrib_right {α : Type u_1} {ι : Type u_4} [distrib_lattice α] [order_top α] (s : finset ι) (f : ι → α) (a : α) :
s.inf f a = s.inf (λ (i : ι), f i a)
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
theorem finset.inf_id_eq_Inf {α : Type u_1} [complete_lattice α] (s : finset α) :
theorem finset.inf_id_set_eq_sInter {α : Type u_1} (s : finset (set α)) :
@[simp]
theorem finset.inf_set_eq_bInter {α : Type u_1} {β : Type u_2} (s : finset α) (f : α → set β) :
s.inf f = ⋂ (x : α) (H : x s), f x
theorem finset.inf_eq_Inf_image {α : Type u_1} {β : Type u_2} [complete_lattice β] (s : finset α) (f : α → β) :
s.inf f = Inf (f '' s)
theorem finset.sup_of_mem {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (f : β → α) {b : β} (h : b s) :
∃ (a : α), s.sup (coe f) = a
def finset.sup' {α : Type u_1} {β : Type u_2} [semilattice_sup α] (s : finset β) (H : s.nonempty) (f : β → α) :
α

Given nonempty finset s then s.sup' H f is the supremum of its image under f in (possibly unbounded) join-semilattice α, where H is a proof of nonemptiness. If α has a bottom element you may instead use finset.sup which does not require s nonempty.

Equations
@[simp]
theorem finset.coe_sup' {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) :
(s.sup' H f) = s.sup (coe f)
@[simp]
theorem finset.sup'_cons {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) {b : β} {hb : b s} {h : (finset.cons b s hb).nonempty} :
(finset.cons b s hb).sup' h f = f b s.sup' H f
@[simp]
theorem finset.sup'_insert {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) [decidable_eq β] {b : β} {h : (insert b s).nonempty} :
(insert b s).sup' h f = f b s.sup' H f
@[simp]
theorem finset.sup'_singleton {α : Type u_1} {β : Type u_2} [semilattice_sup α] (f : β → α) {b : β} {h : {b}.nonempty} :
{b}.sup' h f = f b
theorem finset.sup'_le {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) {a : α} (hs : ∀ (b : β), b sf b a) :
s.sup' H f a
theorem finset.le_sup' {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (f : β → α) {b : β} (h : b s) :
f b s.sup' _ f
@[simp]
theorem finset.sup'_const {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (a : α) :
s.sup' H (λ (b : β), a) = a
@[simp]
theorem finset.sup'_le_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) {a : α} :
s.sup' H f a ∀ (b : β), b sf b a
@[simp]
theorem finset.sup'_lt_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] {a : α} :
s.sup' H f < a ∀ (b : β), b sf b < a
@[simp]
theorem finset.le_sup'_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] {a : α} :
a s.sup' H f ∃ (b : β) (H : b s), a f b
@[simp]
theorem finset.lt_sup'_iff {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] {a : α} :
a < s.sup' H f ∃ (b : β) (H : b s), a < f b
theorem finset.sup'_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] (f : β → α) [decidable_eq β] {s : finset γ} (Hs : s.nonempty) {t : γ → finset β} (Ht : ∀ (b : γ), (t b).nonempty) :
(s.bUnion t).sup' _ f = s.sup' Hs (λ (b : γ), (t b).sup' _ f)
theorem finset.comp_sup'_eq_sup'_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] [semilattice_sup γ] {s : finset β} (H : s.nonempty) {f : β → α} (g : α → γ) (g_sup : ∀ (x y : α), g (x y) = g x g y) :
g (s.sup' H f) = s.sup' H (g f)
theorem finset.sup'_induction {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) {p : α → Prop} (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : ∀ (b : β), b sp (f b)) :
p (s.sup' H f)
theorem finset.exists_mem_eq_sup' {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] :
∃ (b : β), b s s.sup' H f = f b
theorem finset.sup'_mem {α : Type u_1} [semilattice_sup α] (s : set α) (w : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : finset ι) (H : t.nonempty) (p : ι → α) (h : ∀ (i : ι), i tp i s) :
t.sup' H p s
theorem finset.sup'_congr {α : Type u_1} {β : Type u_2} [semilattice_sup α] {s : finset β} (H : s.nonempty) {t : finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ (x : β), x sf x = g x) :
s.sup' H f = t.sup' _ g
theorem finset.inf_of_mem {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (f : β → α) {b : β} (h : b s) :
∃ (a : α), s.inf (coe f) = a
def finset.inf' {α : Type u_1} {β : Type u_2} [semilattice_inf α] (s : finset β) (H : s.nonempty) (f : β → α) :
α

Given nonempty finset s then s.inf' H f is the infimum of its image under f in (possibly unbounded) meet-semilattice α, where H is a proof of nonemptiness. If α has a top element you may instead use finset.inf which does not require s nonempty.

Equations
@[simp]
theorem finset.coe_inf' {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) :
(s.inf' H f) = s.inf (coe f)
@[simp]
theorem finset.inf'_cons {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) {b : β} {hb : b s} {h : (finset.cons b s hb).nonempty} :
(finset.cons b s hb).inf' h f = f b s.inf' H f
@[simp]
theorem finset.inf'_insert {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) [decidable_eq β] {b : β} {h : (insert b s).nonempty} :
(insert b s).inf' h f = f b s.inf' H f
@[simp]
theorem finset.inf'_singleton {α : Type u_1} {β : Type u_2} [semilattice_inf α] (f : β → α) {b : β} {h : {b}.nonempty} :
{b}.inf' h f = f b
theorem finset.le_inf' {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) {a : α} (hs : ∀ (b : β), b sa f b) :
a s.inf' H f
theorem finset.inf'_le {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (f : β → α) {b : β} (h : b s) :
s.inf' _ f f b
@[simp]
theorem finset.inf'_const {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (a : α) :
s.inf' H (λ (b : β), a) = a
@[simp]
theorem finset.le_inf'_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) {a : α} :
a s.inf' H f ∀ (b : β), b sa f b
@[simp]
theorem finset.lt_inf'_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] {a : α} :
a < s.inf' H f ∀ (b : β), b sa < f b
@[simp]
theorem finset.inf'_le_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] {a : α} :
s.inf' H f a ∃ (b : β) (H : b s), f b a
@[simp]
theorem finset.inf'_lt_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] {a : α} :
s.inf' H f < a ∃ (b : β) (H : b s), f b < a
theorem finset.inf'_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] (f : β → α) [decidable_eq β] {s : finset γ} (Hs : s.nonempty) {t : γ → finset β} (Ht : ∀ (b : γ), (t b).nonempty) :
(s.bUnion t).inf' _ f = s.inf' Hs (λ (b : γ), (t b).inf' _ f)
theorem finset.comp_inf'_eq_inf'_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_inf α] [semilattice_inf γ] {s : finset β} (H : s.nonempty) {f : β → α} (g : α → γ) (g_inf : ∀ (x y : α), g (x y) = g x g y) :
g (s.inf' H f) = s.inf' H (g f)
theorem finset.inf'_induction {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) {p : α → Prop} (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : ∀ (b : β), b sp (f b)) :
p (s.inf' H f)
theorem finset.exists_mem_eq_inf' {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β → α) [is_total α has_le.le] :
∃ (b : β), b s s.inf' H f = f b
theorem finset.inf'_mem {α : Type u_1} [semilattice_inf α] (s : set α) (w : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : finset ι) (H : t.nonempty) (p : ι → α) (h : ∀ (i : ι), i tp i s) :
t.inf' H p s
theorem finset.inf'_congr {α : Type u_1} {β : Type u_2} [semilattice_inf α] {s : finset β} (H : s.nonempty) {t : finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ (x : β), x sf x = g x) :
s.inf' H f = t.inf' _ g
theorem finset.sup'_eq_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} (H : s.nonempty) (f : β → α) :
s.sup' H f = s.sup f
theorem finset.sup_closed_of_sup_closed {α : Type u_1} [semilattice_sup α] [order_bot α] {s : set α} (t : finset α) (htne : t.nonempty) (h_subset : t s) (h : ∀ (a : α), a s∀ (b : α), b sa b s) :
t.sup id s
theorem finset.exists_mem_eq_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] [is_total α has_le.le] (s : finset β) (h : s.nonempty) (f : β → α) :
∃ (b : β), b s s.sup f = f b
theorem finset.coe_sup_of_nonempty {α : Type u_1} {β : Type u_2} [semilattice_sup α] [order_bot α] {s : finset β} (h : s.nonempty) (f : β → α) :
(s.sup f) = s.sup (coe f)
theorem finset.inf'_eq_inf {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} (H : s.nonempty) (f : β → α) :
s.inf' H f = s.inf f
theorem finset.inf_closed_of_inf_closed {α : Type u_1} [semilattice_inf α] [order_top α] {s : set α} (t : finset α) (htne : t.nonempty) (h_subset : t s) (h : ∀ (a : α), a s∀ (b : α), b sa b s) :
t.inf id s
theorem finset.exists_mem_eq_inf {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] [is_total α has_le.le] (s : finset β) (h : s.nonempty) (f : β → α) :
∃ (a : β), a s s.inf f = f a
theorem finset.coe_inf_of_nonempty {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_top α] {s : finset β} (h : s.nonempty) (f : β → α) :
(s.inf f) = s.inf (λ (i : β), (f i))
@[protected, simp]
theorem finset.sup_apply {α : Type u_1} {β : Type u_2} {C : β → Type u_5} [Π (b : β), semilattice_sup (C b)] [Π (b : β), order_bot (C b)] (s : finset α) (f : α → Π (b : β), C b) (b : β) :
s.sup f b = s.sup (λ (a : α), f a b)
@[protected, simp]
theorem finset.inf_apply {α : Type u_1} {β : Type u_2} {C : β → Type u_5} [Π (b : β), semilattice_inf (C b)] [Π (b : β), order_top (C b)] (s : finset α) (f : α → Π (b : β), C b) (b : β) :
s.inf f b = s.inf (λ (a : α), f a b)
@[protected, simp]
theorem finset.sup'_apply {α : Type u_1} {β : Type u_2} {C : β → Type u_5} [Π (b : β), semilattice_sup (C b)] {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
s.sup' H f b = s.sup' H (λ (a : α), f a b)
@[protected, simp]
theorem finset.inf'_apply {α : Type u_1} {β : Type u_2} {C : β → Type u_5} [Π (b : β), semilattice_inf (C b)] {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
s.inf' H f b = s.inf' H (λ (a : α), f a b)

max and min of finite sets #

@[protected]
def finset.max {α : Type u_1} [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
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 α} :
@[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 : α} (h : a s) :
∃ (b : α), b s.max
theorem finset.max_of_nonempty {α : Type u_1} [linear_order α] {s : finset α} (h : 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 : α} (h₁ : a s) (h₂ : b s.max) :
a b
@[protected]
def finset.min {α : Type u_1} [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
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 α} :
@[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 : α} (h : a s) :
∃ (b : α), b s.min
theorem finset.min_of_nonempty {α : Type u_1} [linear_order α] {s : finset α} (h : 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 : α} (h₁ : b s) (h₂ : a s.min) :
a b
def finset.min' {α : Type u_1} [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
def finset.max' {α : Type u_1} [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
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 : α) (H2 : ∀ (y : α), y sx y) :
x s.min' H
theorem finset.is_least_min' {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) :
@[simp]
theorem finset.le_min'_iff {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
x s.min' H ∀ (y : α), y sx y
@[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 : α) (H2 : ∀ (y : α), y sy x) :
s.max' H x
theorem finset.is_greatest_max' {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) :
@[simp]
theorem finset.max'_le_iff {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
s.max' H x ∀ (y : α), y sy x
@[simp]
theorem finset.max'_lt_iff {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
s.max' H < x ∀ (y : α), y sy < x
@[simp]
theorem finset.lt_min'_iff {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
x < s.min' H ∀ (y : α), y sx < y
theorem finset.max'_eq_sup' {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) :
s.max' H = s.sup' H id
theorem finset.min'_eq_inf' {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) :
s.min' H = s.inf' H id
@[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) (H2 : j s) (H3 : i j) :
s.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'_subset {α : Type u_1} [linear_order α] {s t : finset α} (H : s.nonempty) (hst : s t) :
s.max' H t.max' _
theorem finset.min'_subset {α : Type u_1} [linear_order α] {s t : finset α} (H : s.nonempty) (hst : s t) :
t.min' _ s.min' H
theorem finset.max'_insert {α : Type u_1} [linear_order α] (a : α) (s : finset α) (H : s.nonempty) :
(insert a s).max' _ = max (s.max' H) a
theorem finset.min'_insert {α : Type u_1} [linear_order α] (a : α) (s : finset α) (H : s.nonempty) :
(insert a s).min' _ = min (s.min' H) a
theorem finset.lt_max'_of_mem_erase_max' {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) [decidable_eq α] {a : α} (ha : a s.erase (s.max' H)) :
a < s.max' H
theorem finset.min'_lt_of_mem_erase_min' {α : Type u_1} [linear_order α] (s : finset α) (H : s.nonempty) [decidable_eq α] {a : α} (ha : a s.erase (s.min' H)) :
s.min' H < a
@[simp]
theorem finset.max'_image {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {f : α → β} (hf : monotone f) (s : finset α) (h : (finset.image f s).nonempty) :
(finset.image f s).max' h = f (s.max' _)
@[simp]
theorem finset.min'_image {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {f : α → β} (hf : monotone f) (s : finset α) (h : (finset.image f s).nonempty) :
(finset.image f s).min' h = f (s.min' _)
theorem finset.induction_on_max {α : Type u_1} [linear_order α] [decidable_eq α] {p : finset α → Prop} (s : finset α) (h0 : p ) (step : ∀ (a : α) (s : finset α), (∀ (x : α), x sx < a)p sp (insert a s)) :
p s

Induction principle for finsets in a linearly ordered type: a predicate is true on all s : finset α provided that:

  • it is true on the empty finset,
  • for every s : finset α and an element a strictly greater than all elements of s, p s implies p (insert a s).
theorem finset.induction_on_min {α : Type u_1} [linear_order α] [decidable_eq α] {p : finset α → Prop} (s : finset α) (h0 : p ) (step : ∀ (a : α) (s : finset α), (∀ (x : α), x sa < x)p sp (insert a s)) :
p s

Induction principle for finsets in a linearly ordered type: a predicate is true on all s : finset α provided that:

  • it is true on the empty finset,
  • for every s : finset α and an element a strictly less than all elements of s, p s implies p (insert a s).
theorem finset.induction_on_max_value {α : Type u_1} {ι : Type u_4} [linear_order α] [decidable_eq ι] (f : ι → α) {p : finset ι → Prop} (s : finset ι) (h0 : p ) (step : ∀ (a : ι) (s : finset ι), a s(∀ (x : ι), x sf x f a)p sp (insert a s)) :
p s

Induction principle for finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : finset α provided that:

  • it is true on the empty finset,
  • for every s : finset α and an element a such that for elements of s denoted by x we have f x ≤ f a, p s implies p (insert a s).
theorem finset.induction_on_min_value {α : Type u_1} {ι : Type u_4} [linear_order α] [decidable_eq ι] (f : ι → α) {p : finset ι → Prop} (s : finset ι) (h0 : p ) (step : ∀ (a : ι) (s : finset ι), a s(∀ (x : ι), x sf a f x)p sp (insert a s)) :
p s

Induction principle for finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : finset α provided that:

  • it is true on the empty finset,
  • for every s : finset α and an element a such that for elements of s denoted by x we have f a ≤ f x, p s implies p (insert a s).
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' sf x' f x
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' sf x f x'
theorem multiset.map_finset_sup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] [decidable_eq β] (s : finset γ) (f : γ → multiset β) (g : β → α) (hg : function.injective g) :
theorem multiset.count_finset_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))
theorem multiset.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
theorem finset.mem_sup {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α → finset β} {x : β} :
x s.sup f ∃ (v : α) (H : v s), x f v
theorem finset.sup_eq_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (t : α → finset β) :
s.sup t = s.bUnion t
@[simp]
theorem finset.sup_singleton'' {α : Type u_1} {β : Type u_2} [decidable_eq α] (s : finset β) (f : β → α) :
s.sup (λ (b : β), {f b}) = finset.image f s
@[simp]
theorem finset.sup_singleton' {α : Type u_1} [decidable_eq α] (s : finset α) :
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*.

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.

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

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.

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 ordered algebra structures #

theorem finset.sup_mul_le_mul_sup_of_nonneg {α : Type u_1} {ι : Type u_4} [linear_ordered_semiring α] [order_bot α] {a b : ι → α} (s : finset ι) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
s.sup (a * b) (s.sup a) * s.sup b
theorem finset.mul_inf_le_inf_mul_of_nonneg {α : Type u_1} {ι : Type u_4} [linear_ordered_semiring α] [order_top α] {a b : ι → α} (s : finset ι) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
(s.inf a) * s.inf b s.inf (a * b)
theorem finset.sup'_mul_le_mul_sup'_of_nonneg {α : Type u_1} {ι : Type u_4} [linear_ordered_semiring α] {a b : ι → α} (s : finset ι) (H : s.nonempty) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
s.sup' H (a * b) (s.sup' H a) * s.sup' H b
theorem finset.inf'_mul_le_mul_inf'_of_nonneg {α : Type u_1} {ι : Type u_4} [linear_ordered_semiring α] {a b : ι → α} (s : finset ι) (H : s.nonempty) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
(s.inf' H a) * s.inf' H b s.inf' H (a * b)

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} [complete_lattice β] (a : α) (s : α → β) :
(⨆ (x : α) (H : x {a}), s x) = s a
theorem finset.infi_singleton {α : Type u_1} {β : Type u_2} [complete_lattice β] (a : α) (s : α → β) :
(⨅ (x : α) (H : x {a}), s x) = s a
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
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
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
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
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
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
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)
theorem finset.sup_finset_image {α : Type u_1} [decidable_eq α] {β : Type u_2} {γ : Type u_3} [semilattice_sup β] [order_bot β] (f : γ → α) (g : α → β) (s : finset γ) :
(finset.image f s).sup g = s.sup (g f)
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)
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
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
theorem finset.supr_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [complete_lattice β] [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → β) :
(⨆ (y : α) (H : y s.bUnion t), f y) = ⨆ (x : γ) (H : x s) (y : α) (H : y t x), f y
theorem finset.infi_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [complete_lattice β] [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → β) :
(⨅ (y : α) (H : y s.bUnion t), f y) = ⨅ (x : γ) (H : x s) (y : α) (H : y t x), f y
theorem finset.set_bUnion_coe {α : Type u_1} {β : Type u_2} (s : finset α) (t : α → set β) :
(⋃ (x : α) (H : x s), t x) = ⋃ (x : α) (H : x s), t x
theorem finset.set_bInter_coe {α : Type u_1} {β : Type u_2} (s : finset α) (t : α → set β) :
(⋂ (x : α) (H : x s), t x) = ⋂ (x : α) (H : x s), t x
theorem finset.set_bUnion_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → set β) :
(⋃ (x : α) (H : x {a}), s x) = s a
theorem finset.set_bInter_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → set β) :
(⋂ (x : α) (H : x {a}), s x) = s a
@[simp]
theorem finset.set_bUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (s : finset β) :
(⋃ (y : β) (H : y s), f ⁻¹' {y}) = f ⁻¹' s
theorem finset.set_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
theorem finset.set_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.subset_set_bUnion_of_mem {α : Type u_1} {β : Type u_2} {s : finset α} {f : α → set β} {x : α} (h : x s) :
f x ⋃ (y : α) (H : y s), f y
theorem finset.set_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.set_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
theorem finset.set_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
theorem finset.set_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
theorem finset.set_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)
theorem finset.set_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)
theorem finset.set_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
theorem finset.set_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
theorem finset.set_bUnion_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → set β) :
(⋃ (y : α) (H : y s.bUnion t), f y) = ⋃ (x : γ) (H : x s) (y : α) (H : y t x), f y
theorem finset.set_bInter_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] (s : finset γ) (t : γ → finset α) (f : α → set β) :
(⋂ (y : α) (H : y s.bUnion t), f y) = ⋂ (x : γ) (H : x s) (y : α) (H : y t x), f y