mathlib3 documentation

data.finset.lattice

Lattice operations on finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

sup #

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

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

Equations
Instances for finset.sup
theorem finset.sup_def {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f : β α} :
@[simp]
theorem finset.sup_empty {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {f : β α} :
@[simp]
theorem finset.sup_cons {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f : β α} [decidable_eq β] {b : β} :
(has_insert.insert b s).sup f = f b s.sup f
theorem finset.sup_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {f : β α} {b : β} :
{b}.sup f = f b
theorem finset.sup_union {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f g : β α} :
s.sup (f g) = s.sup f s.sup g
theorem finset.sup_congr {α : Type u_2} {β : Type u_3} [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 map_finset_sup {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [semilattice_sup α] [order_bot α] [semilattice_sup β] [order_bot β] [sup_bot_hom_class F α β] (f : F) (s : finset ι) (g : ι α) :
f (s.sup g) = s.sup (f g)
@[protected, simp]
theorem finset.sup_le_iff {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f : β α} {a : α} :
s.sup f a (b : β), b s f b a
@[protected]
theorem finset.sup_le {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f : β α} {a : α} :
( (b : β), b s f b a) s.sup f a

Alias of the reverse direction of finset.sup_le_iff.

theorem finset.sup_const_le {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {a : α} :
s.sup (λ (_x : β), a) a
theorem finset.le_sup {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f : β α} {b : β} (hb : b s) :
f b s.sup f
theorem finset.le_sup_of_le {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f : β α} {a : α} {b : β} (hb : b s) (h : a f b) :
a s.sup f
@[simp]
theorem finset.sup_bUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} (h : s.nonempty) (c : α) :
s.sup (λ (_x : β), c) = c
@[simp]
theorem finset.sup_bot {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] (s : finset β) :
s.sup (λ (_x : β), ) =
theorem finset.sup_ite {α : Type u_2} {β : Type u_3} [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_mono_fun {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f g : β α} (h : (b : β), b s f b g b) :
s.sup f s.sup g
theorem finset.sup_mono {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s₁ s₂ : finset β} {f : β α} (h : s₁ s₂) :
s₁.sup f s₂.sup f
@[protected]
theorem finset.sup_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [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_2} {β : Type u_3} {γ : Type u_4} [semilattice_sup α] [order_bot α] (s : finset β) (t : finset γ) (f : β × γ α) :
(s ×ˢ t).sup f = s.sup (λ (i : β), t.sup (λ (i' : γ), f (i, i')))

See also finset.product_bUnion.

theorem finset.sup_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [semilattice_sup α] [order_bot α] (s : finset β) (t : finset γ) (f : β × γ α) :
(s ×ˢ t).sup f = t.sup (λ (i' : γ), s.sup (λ (i : β), f (i, i')))
@[simp]
theorem finset.sup_erase_bot {α : Type u_2} [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_2} {β : Type u_3} {γ : Type u_4} [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.sup_coe {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_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))

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_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} {f : β α} {p : α Prop} (hb : p ) (hp : (a₁ : α), p a₁ (a₂ : α), p a₂ p (a₁ a₂)) (hs : (b : β), b s p (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_2} [semilattice_sup α] [order_bot α] (s : set α) (w₁ : s) (w₂ : (x : α), x s (y : α), y s x y s) {ι : Type u_1} (t : finset ι) (p : ι α) (h : (i : ι), i t p i s) :
t.sup p s
@[protected, simp]
theorem finset.sup_eq_bot_iff {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] (f : β α) (S : finset β) :
S.sup f = (s : β), s S f s =
theorem finset.sup_eq_supr {α : Type u_2} {β : Type u_3} [complete_lattice β] (s : finset α) (f : α β) :
s.sup f = (a : α) (H : a s), f a
theorem finset.sup_id_eq_Sup {α : Type u_2} [complete_lattice α] (s : finset α) :
theorem finset.sup_id_set_eq_sUnion {α : Type u_2} (s : finset (set α)) :
@[simp]
theorem finset.sup_set_eq_bUnion {α : Type u_2} {β : Type u_3} (s : finset α) (f : α set β) :
s.sup f = (x : α) (H : x s), f x
theorem finset.sup_eq_Sup_image {α : Type u_2} {β : Type u_3} [complete_lattice β] (s : finset α) (f : α β) :

inf #

def finset.inf {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f : β α} :
@[simp]
theorem finset.inf_empty {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {f : β α} :
@[simp]
theorem finset.inf_cons {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f : β α} [decidable_eq β] {b : β} :
(has_insert.insert b s).inf f = f b s.inf f
theorem finset.inf_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [semilattice_inf α] [order_top α] {f : β α} {b : β} :
{b}.inf f = f b
theorem finset.inf_union {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f g : β α} :
s.inf (f g) = s.inf f s.inf g
theorem finset.inf_congr {α : Type u_2} {β : Type u_3} [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 map_finset_inf {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [semilattice_inf α] [order_top α] [semilattice_inf β] [order_top β] [inf_top_hom_class F α β] (f : F) (s : finset ι) (g : ι α) :
f (s.inf g) = s.inf (f g)
@[simp]
theorem finset.inf_bUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} (h : s.nonempty) (c : α) :
s.inf (λ (_x : β), c) = c
@[simp]
theorem finset.inf_top {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] (s : finset β) :
s.inf (λ (_x : β), ) =
@[protected]
theorem finset.le_inf_iff {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f : β α} {a : α} :
a s.inf f (b : β), b s a f b
@[protected]
theorem finset.le_inf {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f : β α} {a : α} :
( (b : β), b s a f b) a s.inf f

Alias of the reverse direction of finset.le_inf_iff.

theorem finset.le_inf_const_le {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {a : α} :
a s.inf (λ (_x : β), a)
theorem finset.inf_le {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f : β α} {b : β} (hb : b s) :
s.inf f f b
theorem finset.inf_le_of_le {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f : β α} {a : α} {b : β} (hb : b s) (h : f b a) :
s.inf f a
theorem finset.inf_mono_fun {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f g : β α} (h : (b : β), b s f b g b) :
s.inf f s.inf g
theorem finset.inf_mono {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s₁ s₂ : finset β} {f : β α} (h : s₁ s₂) :
s₂.inf f s₁.inf f
theorem finset.inf_attach {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] (s : finset β) (f : β α) :
s.attach.inf (λ (x : {x // x s}), f x) = s.inf f
@[protected]
theorem finset.inf_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [semilattice_inf α] [order_top α] (s : finset β) (t : finset γ) (f : β × γ α) :
(s ×ˢ t).inf f = s.inf (λ (i : β), t.inf (λ (i' : γ), f (i, i')))
theorem finset.inf_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [semilattice_inf α] [order_top α] (s : finset β) (t : finset γ) (f : β × γ α) :
(s ×ˢ t).inf f = t.inf (λ (i' : γ), s.inf (λ (i : β), f (i, i')))
@[simp]
theorem finset.inf_erase_top {α : Type u_2} [semilattice_inf α] [order_top α] [decidable_eq α] (s : finset α) :
theorem finset.comp_inf_eq_inf_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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.inf_coe {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_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))

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

theorem finset.inf_induction {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] {s : finset β} {f : β α} {p : α Prop} (ht : p ) (hp : (a₁ : α), p a₁ (a₂ : α), p a₂ p (a₁ a₂)) (hs : (b : β), b s p (f b)) :
p (s.inf f)
theorem finset.inf_mem {α : Type u_2} [semilattice_inf α] [order_top α] (s : set α) (w₁ : s) (w₂ : (x : α), x s (y : α), y s x y s) {ι : Type u_1} (t : finset ι) (p : ι α) (h : (i : ι), i t p i s) :
t.inf p s
@[protected, simp]
theorem finset.inf_eq_top_iff {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] (f : β α) (S : finset β) :
S.inf f = (s : β), s S f s =
@[simp]
theorem finset.to_dual_sup {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] (s : finset β) (f : β α) :
@[simp]
theorem finset.to_dual_inf {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] (s : finset β) (f : β α) :
@[simp]
theorem finset.of_dual_sup {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_top α] (s : finset β) (f : β αᵒᵈ) :
@[simp]
theorem finset.of_dual_inf {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] (s : finset β) (f : β αᵒᵈ) :
theorem finset.sup_inf_distrib_left {α : Type u_2} {ι : Type u_5} [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_2} {ι : Type u_5} [distrib_lattice α] [order_bot α] (s : finset ι) (f : ι α) (a : α) :
s.sup f a = s.sup (λ (i : ι), f i a)
@[protected]
theorem finset.disjoint_sup_right {α : Type u_2} {ι : Type u_5} [distrib_lattice α] [order_bot α] {s : finset ι} {f : ι α} {a : α} :
disjoint a (s.sup f) ⦃i : ι⦄, i s disjoint a (f i)
@[protected]
theorem finset.disjoint_sup_left {α : Type u_2} {ι : Type u_5} [distrib_lattice α] [order_bot α] {s : finset ι} {f : ι α} {a : α} :
disjoint (s.sup f) a ⦃i : ι⦄, i s disjoint (f i) a
theorem finset.sup_inf_sup {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [distrib_lattice α] [order_bot α] (s : finset ι) (t : finset κ) (f : ι α) (g : κ α) :
s.sup f t.sup g = (s ×ˢ t).sup (λ (i : ι × κ), f i.fst g i.snd)
theorem finset.inf_sup_distrib_left {α : Type u_2} {ι : Type u_5} [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_2} {ι : Type u_5} [distrib_lattice α] [order_top α] (s : finset ι) (f : ι α) (a : α) :
s.inf f a = s.inf (λ (i : ι), f i a)
@[protected]
theorem finset.codisjoint_inf_right {α : Type u_2} {ι : Type u_5} [distrib_lattice α] [order_top α] {f : ι α} {s : finset ι} {a : α} :
codisjoint a (s.inf f) ⦃i : ι⦄, i s codisjoint a (f i)
@[protected]
theorem finset.codisjoint_inf_left {α : Type u_2} {ι : Type u_5} [distrib_lattice α] [order_top α] {f : ι α} {s : finset ι} {a : α} :
codisjoint (s.inf f) a ⦃i : ι⦄, i s codisjoint (f i) a
theorem finset.inf_sup_inf {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [distrib_lattice α] [order_top α] (s : finset ι) (t : finset κ) (f : ι α) (g : κ α) :
s.inf f t.inf g = (s ×ˢ t).inf (λ (i : ι × κ), f i.fst g i.snd)
theorem finset.inf_sup {α : Type u_2} {ι : Type u_5} [distrib_lattice α] [bounded_order α] [decidable_eq ι] {κ : ι Type u_1} (s : finset ι) (t : Π (i : ι), finset (κ i)) (f : Π (i : ι), κ i α) :
s.inf (λ (i : ι), (t i).sup (f i)) = (s.pi t).sup (λ (g : Π (a : ι), a s κ a), s.attach.inf (λ (i : {x // x s}), f i (g i _)))
theorem finset.sup_inf {α : Type u_2} {ι : Type u_5} [distrib_lattice α] [bounded_order α] [decidable_eq ι] {κ : ι Type u_1} (s : finset ι) (t : Π (i : ι), finset (κ i)) (f : Π (i : ι), κ i α) :
s.sup (λ (i : ι), (t i).inf (f i)) = (s.pi t).inf (λ (g : Π (a : ι), a s κ a), s.attach.sup (λ (i : {x // x s}), f i.val (g i.val _)))
theorem finset.sup_sdiff_left {α : Type u_2} {ι : Type u_5} [boolean_algebra α] (s : finset ι) (f : ι α) (a : α) :
s.sup (λ (b : ι), a \ f b) = a \ s.inf f
theorem finset.inf_sdiff_left {α : Type u_2} {ι : Type u_5} [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_2} {ι : Type u_5} [boolean_algebra α] {s : finset ι} (hs : s.nonempty) (f : ι α) (a : α) :
s.inf (λ (b : ι), f b \ a) = s.inf f \ a
theorem finset.inf_himp_right {α : Type u_2} {ι : Type u_5} [boolean_algebra α] (s : finset ι) (f : ι α) (a : α) :
s.inf (λ (b : ι), f b a) = s.sup f a
theorem finset.sup_himp_right {α : Type u_2} {ι : Type u_5} [boolean_algebra α] {s : finset ι} (hs : s.nonempty) (f : ι α) (a : α) :
s.sup (λ (b : ι), f b a) = s.inf f a
theorem finset.sup_himp_left {α : Type u_2} {ι : Type u_5} [boolean_algebra α] {s : finset ι} (hs : s.nonempty) (f : ι α) (a : α) :
s.sup (λ (b : ι), a f b) = a s.sup f
@[protected, simp]
theorem finset.compl_sup {α : Type u_2} {ι : Type u_5} [boolean_algebra α] (s : finset ι) (f : ι α) :
(s.sup f) = s.inf (λ (i : ι), (f i))
@[protected, simp]
theorem finset.compl_inf {α : Type u_2} {ι : Type u_5} [boolean_algebra α] (s : finset ι) (f : ι α) :
(s.inf f) = s.sup (λ (i : ι), (f i))
theorem finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [linear_order α] [order_bot α] {s : finset ι} {f : ι α} [semilattice_sup β] [order_bot β] (g : α β) (mono_g : monotone g) (bot : g = ) :
g (s.sup f) = s.sup (g f)
@[protected, simp]
theorem finset.le_sup_iff {α : Type u_2} {ι : Type u_5} [linear_order α] [order_bot α] {s : finset ι} {f : ι α} {a : α} (ha : < a) :
a s.sup f (b : ι) (H : b s), a f b
@[protected, simp]
theorem finset.lt_sup_iff {α : Type u_2} {ι : Type u_5} [linear_order α] [order_bot α] {s : finset ι} {f : ι α} {a : α} :
a < s.sup f (b : ι) (H : b s), a < f b
@[protected, simp]
theorem finset.sup_lt_iff {α : Type u_2} {ι : Type u_5} [linear_order α] [order_bot α] {s : finset ι} {f : ι α} {a : α} (ha : < a) :
s.sup f < a (b : ι), b s f b < a
theorem finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [linear_order α] [order_top α] {s : finset ι} {f : ι α} [semilattice_inf β] [order_top β] (g : α β) (mono_g : monotone g) (top : g = ) :
g (s.inf f) = s.inf (g f)
@[protected, simp]
theorem finset.inf_le_iff {α : Type u_2} {ι : Type u_5} [linear_order α] [order_top α] {s : finset ι} {f : ι α} {a : α} (ha : a < ) :
s.inf f a (b : ι) (H : b s), f b a
@[protected, simp]
theorem finset.inf_lt_iff {α : Type u_2} {ι : Type u_5} [linear_order α] [order_top α] {s : finset ι} {f : ι α} {a : α} :
s.inf f < a (b : ι) (H : b s), f b < a
@[protected, simp]
theorem finset.lt_inf_iff {α : Type u_2} {ι : Type u_5} [linear_order α] [order_top α] {s : finset ι} {f : ι α} {a : α} (ha : a < ) :
a < s.inf f (b : ι), b s a < f b
theorem finset.inf_eq_infi {α : Type u_2} {β : Type u_3} [complete_lattice β] (s : finset α) (f : α β) :
s.inf f = (a : α) (H : a s), f a
theorem finset.inf_id_eq_Inf {α : Type u_2} [complete_lattice α] (s : finset α) :
theorem finset.inf_id_set_eq_sInter {α : Type u_2} (s : finset (set α)) :
@[simp]
theorem finset.inf_set_eq_bInter {α : Type u_2} {β : Type u_3} (s : finset α) (f : α set β) :
s.inf f = (x : α) (H : x s), f x
theorem finset.inf_eq_Inf_image {α : Type u_2} {β : Type u_3} [complete_lattice β] (s : finset α) (f : α β) :
theorem finset.sup_of_mem {α : Type u_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (f : β α) {b : β} (h : b s) :
(a : α), s.sup (coe f) = a
def finset.sup' {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β α) :
(s.sup' H f) = s.sup (coe f)
@[simp]
theorem finset.sup'_cons {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β α) [decidable_eq β] {b : β} {h : (has_insert.insert b s).nonempty} :
(has_insert.insert b s).sup' h f = f b s.sup' H f
@[simp]
theorem finset.sup'_singleton {α : Type u_2} {β : Type u_3} [semilattice_sup α] (f : β α) {b : β} {h : {b}.nonempty} :
{b}.sup' h f = f b
theorem finset.sup'_le {α : Type u_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β α) {a : α} (hs : (b : β), b s f b a) :
s.sup' H f a
theorem finset.le_sup' {α : Type u_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (f : β α) {b : β} (h : b s) :
f b s.sup' _ f
theorem finset.le_sup'_of_le {α : Type u_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (f : β α) {a : α} {b : β} (hb : b s) (h : a f b) :
a s.sup' _ f
@[simp]
theorem finset.sup'_const {α : Type u_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (H : s.nonempty) (a : α) :
s.sup' H (λ (b : β), a) = a
@[simp]
theorem finset.sup'_le_iff {α : Type u_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β α) {a : α} :
s.sup' H f a (b : β), b s f b a
theorem finset.sup'_bUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (H : s.nonempty) (f : β α) {p : α Prop} (hp : (a₁ : α), p a₁ (a₂ : α), p a₂ p (a₁ a₂)) (hs : (b : β), b s p (f b)) :
p (s.sup' H f)
theorem finset.sup'_mem {α : Type u_2} [semilattice_sup α] (s : set α) (w : (x : α), x s (y : α), y s x y s) {ι : Type u_1} (t : finset ι) (H : t.nonempty) (p : ι α) (h : (i : ι), i t p i s) :
t.sup' H p s
theorem finset.sup'_congr {α : Type u_2} {β : Type u_3} [semilattice_sup α] {s : finset β} (H : s.nonempty) {t : finset β} {f g : β α} (h₁ : s = t) (h₂ : (x : β), x s f x = g x) :
s.sup' H f = t.sup' _ g
@[simp]
theorem finset.sup'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [semilattice_sup α] {s : finset γ} {f : γ β} (g : β α) (hs : (finset.map f s).nonempty) (hs' : s.nonempty := _) :
(finset.map f s).sup' hs g = s.sup' hs' (g f)
theorem finset.inf_of_mem {α : Type u_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (f : β α) {b : β} (h : b s) :
(a : α), s.inf (coe f) = a
def finset.inf' {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β α) :
(s.inf' H f) = s.inf (coe f)
@[simp]
theorem finset.inf'_cons {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β α) [decidable_eq β] {b : β} {h : (has_insert.insert b s).nonempty} :
(has_insert.insert b s).inf' h f = f b s.inf' H f
@[simp]
theorem finset.inf'_singleton {α : Type u_2} {β : Type u_3} [semilattice_inf α] (f : β α) {b : β} {h : {b}.nonempty} :
{b}.inf' h f = f b
theorem finset.le_inf' {α : Type u_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β α) {a : α} (hs : (b : β), b s a f b) :
a s.inf' H f
theorem finset.inf'_le {α : Type u_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (f : β α) {b : β} (h : b s) :
s.inf' _ f f b
theorem finset.inf'_le_of_le {α : Type u_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (f : β α) {a : α} {b : β} (hb : b s) (h : f b a) :
s.inf' _ f a
@[simp]
theorem finset.inf'_const {α : Type u_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (H : s.nonempty) (a : α) :
s.inf' H (λ (b : β), a) = a
@[simp]
theorem finset.le_inf'_iff {α : Type u_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β α) {a : α} :
a s.inf' H f (b : β), b s a f b
theorem finset.inf'_bUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (H : s.nonempty) (f : β α) {p : α Prop} (hp : (a₁ : α), p a₁ (a₂ : α), p a₂ p (a₁ a₂)) (hs : (b : β), b s p (f b)) :
p (s.inf' H f)
theorem finset.inf'_mem {α : Type u_2} [semilattice_inf α] (s : set α) (w : (x : α), x s (y : α), y s x y s) {ι : Type u_1} (t : finset ι) (H : t.nonempty) (p : ι α) (h : (i : ι), i t p i s) :
t.inf' H p s
theorem finset.inf'_congr {α : Type u_2} {β : Type u_3} [semilattice_inf α] {s : finset β} (H : s.nonempty) {t : finset β} {f g : β α} (h₁ : s = t) (h₂ : (x : β), x s f x = g x) :
s.inf' H f = t.inf' _ g
@[simp]
theorem finset.inf'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [semilattice_inf α] {s : finset γ} {f : γ β} (g : β α) (hs : (finset.map f s).nonempty) (hs' : s.nonempty := _) :
(finset.map f s).inf' hs g = s.inf' hs' (g f)
theorem finset.sup'_eq_sup {α : Type u_2} {β : Type u_3} [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_2} [semilattice_sup α] [order_bot α] {s : set α} (t : finset α) (htne : t.nonempty) (h_subset : t s) (h : (a : α), a s (b : α), b s a b s) :
t.sup id s
theorem finset.coe_sup_of_nonempty {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_bot α] {s : finset β} (h : s.nonempty) (f : β α) :
(s.sup f) = s.sup (coe f)
theorem finset.inf'_eq_inf {α : Type u_2} {β : Type u_3} [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_2} [semilattice_inf α] [order_top α] {s : set α} (t : finset α) (htne : t.nonempty) (h_subset : t s) (h : (a : α), a s (b : α), b s a b s) :
t.inf id s
theorem finset.coe_inf_of_nonempty {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} {C : β Type u_7} [Π (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_2} {β : Type u_3} {C : β Type u_7} [Π (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_2} {β : Type u_3} {C : β Type u_7} [Π (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_2} {β : Type u_3} {C : β Type u_7} [Π (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)
@[simp]
theorem finset.to_dual_sup' {α : Type u_2} {ι : Type u_5} [semilattice_sup α] {s : finset ι} (hs : s.nonempty) (f : ι α) :
@[simp]
theorem finset.to_dual_inf' {α : Type u_2} {ι : Type u_5} [semilattice_inf α] {s : finset ι} (hs : s.nonempty) (f : ι α) :
@[simp]
theorem finset.of_dual_sup' {α : Type u_2} {ι : Type u_5} [semilattice_inf α] {s : finset ι} (hs : s.nonempty) (f : ι αᵒᵈ) :
@[simp]
theorem finset.of_dual_inf' {α : Type u_2} {ι : Type u_5} [semilattice_sup α] {s : finset ι} (hs : s.nonempty) (f : ι αᵒᵈ) :
@[simp]
theorem finset.le_sup'_iff {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) {f : ι α} {a : α} :
a s.sup' H f (b : ι) (H : b s), a f b
@[simp]
theorem finset.lt_sup'_iff {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) {f : ι α} {a : α} :
a < s.sup' H f (b : ι) (H : b s), a < f b
@[simp]
theorem finset.sup'_lt_iff {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) {f : ι α} {a : α} :
s.sup' H f < a (i : ι), i s f i < a
@[simp]
theorem finset.inf'_le_iff {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) {f : ι α} {a : α} :
s.inf' H f a (i : ι) (H : i s), f i a
@[simp]
theorem finset.inf'_lt_iff {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) {f : ι α} {a : α} :
s.inf' H f < a (i : ι) (H : i s), f i < a
@[simp]
theorem finset.lt_inf'_iff {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) {f : ι α} {a : α} :
a < s.inf' H f (i : ι), i s a < f i
theorem finset.exists_mem_eq_sup' {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) (f : ι α) :
(i : ι), i s s.sup' H f = f i
theorem finset.exists_mem_eq_inf' {α : Type u_2} {ι : Type u_5} [linear_order α] {s : finset ι} (H : s.nonempty) (f : ι α) :
(i : ι), i s s.inf' H f = f i
theorem finset.exists_mem_eq_sup {α : Type u_2} {ι : Type u_5} [linear_order α] [order_bot α] (s : finset ι) (h : s.nonempty) (f : ι α) :
(i : ι), i s s.sup f = f i
theorem finset.exists_mem_eq_inf {α : Type u_2} {ι : Type u_5} [linear_order α] [order_top α] (s : finset ι) (h : s.nonempty) (f : ι α) :
(i : ι), i s s.inf f = f i

max and min of finite sets #

@[protected]
def finset.max {α : Type u_2} [linear_order α] (s : finset α) :

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

Equations
theorem finset.max_eq_sup_coe {α : Type u_2} [linear_order α] {s : finset α} :
s.max = s.sup coe
theorem finset.max_eq_sup_with_bot {α : Type u_2} [linear_order α] (s : finset α) :
s.max = s.sup coe
@[simp]
theorem finset.max_empty {α : Type u_2} [linear_order α] :
@[simp]
theorem finset.max_insert {α : Type u_2} [linear_order α] {a : α} {s : finset α} :
@[simp]
theorem finset.max_singleton {α : Type u_2} [linear_order α] {a : α} :
{a}.max = a
theorem finset.max_of_mem {α : Type u_2} [linear_order α] {s : finset α} {a : α} (h : a s) :
(b : α), s.max = b
theorem finset.max_of_nonempty {α : Type u_2} [linear_order α] {s : finset α} (h : s.nonempty) :
(a : α), s.max = a
theorem finset.max_eq_bot {α : Type u_2} [linear_order α] {s : finset α} :
theorem finset.mem_of_max {α : Type u_2} [linear_order α] {s : finset α} {a : α} :
s.max = a a s
theorem finset.le_max {α : Type u_2} [linear_order α] {a : α} {s : finset α} (as : a s) :
theorem finset.not_mem_of_max_lt_coe {α : Type u_2} [linear_order α] {a : α} {s : finset α} (h : s.max < a) :
a s
theorem finset.le_max_of_eq {α : Type u_2} [linear_order α] {s : finset α} {a b : α} (h₁ : a s) (h₂ : s.max = b) :
a b
theorem finset.not_mem_of_max_lt {α : Type u_2} [linear_order α] {s : finset α} {a b : α} (h₁ : b < a) (h₂ : s.max = b) :
a s
theorem finset.max_mono {α : Type u_2} [linear_order α] {s t : finset α} (st : s t) :
s.max t.max
@[protected]
theorem finset.max_le {α : Type u_2} [linear_order α] {M : with_bot α} {s : finset α} (st : (a : α), a s a M) :
s.max M
@[protected]
def finset.min {α : Type u_2} [linear_order α] (s : finset α) :

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

Equations
theorem finset.min_eq_inf_with_top {α : Type u_2} [linear_order α] (s : finset α) :
s.min = s.inf coe
@[simp]
theorem finset.min_empty {α : Type u_2} [linear_order α] :
@[simp]
theorem finset.min_insert {α : Type u_2} [linear_order α] {a : α} {s : finset α} :
@[simp]
theorem finset.min_singleton {α : Type u_2} [linear_order α] {a : α} :
{a}.min = a
theorem finset.min_of_mem {α : Type u_2} [linear_order α] {s : finset α} {a : α} (h : a s) :
(b : α), s.min = b
theorem finset.min_of_nonempty {α : Type u_2} [linear_order α] {s : finset α} (h : s.nonempty) :
(a : α), s.min = a
theorem finset.min_eq_top {α : Type u_2} [linear_order α] {s : finset α} :
theorem finset.mem_of_min {α : Type u_2} [linear_order α] {s : finset α} {a : α} :
s.min = a a s
theorem finset.min_le {α : Type u_2} [linear_order α] {a : α} {s : finset α} (as : a s) :
theorem finset.not_mem_of_coe_lt_min {α : Type u_2} [linear_order α] {a : α} {s : finset α} (h : a < s.min) :
a s
theorem finset.min_le_of_eq {α : Type u_2} [linear_order α] {s : finset α} {a b : α} (h₁ : b s) (h₂ : s.min = a) :
a b
theorem finset.not_mem_of_lt_min {α : Type u_2} [linear_order α] {s : finset α} {a b : α} (h₁ : a < b) (h₂ : s.min = b) :
a s
theorem finset.min_mono {α : Type u_2} [linear_order α] {s t : finset α} (st : s t) :
t.min s.min
@[protected]
theorem finset.le_min {α : Type u_2} [linear_order α] {m : with_top α} {s : finset α} (st : (a : α), a s m a) :
m s.min
def finset.min' {α : Type u_2} [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 with_top α.

Equations
def finset.max' {α : Type u_2} [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 with_bot α.

Equations
theorem finset.min'_mem {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) :
s.min' H s
theorem finset.min'_le {α : Type u_2} [linear_order α] (s : finset α) (x : α) (H2 : x s) :
s.min' _ x
theorem finset.le_min' {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) (x : α) (H2 : (y : α), y s x y) :
x s.min' H
theorem finset.is_least_min' {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) :
@[simp]
theorem finset.le_min'_iff {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
x s.min' H (y : α), y s x y
@[simp]
theorem finset.min'_singleton {α : Type u_2} [linear_order α] (a : α) :
{a}.min' _ = a

{a}.min' _ is a.

theorem finset.max'_mem {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) :
s.max' H s
theorem finset.le_max' {α : Type u_2} [linear_order α] (s : finset α) (x : α) (H2 : x s) :
x s.max' _
theorem finset.max'_le {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) (x : α) (H2 : (y : α), y s y x) :
s.max' H x
theorem finset.is_greatest_max' {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) :
@[simp]
theorem finset.max'_le_iff {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
s.max' H x (y : α), y s y x
@[simp]
theorem finset.max'_lt_iff {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
s.max' H < x (y : α), y s y < x
@[simp]
theorem finset.lt_min'_iff {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) {x : α} :
x < s.min' H (y : α), y s x < y
theorem finset.max'_eq_sup' {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) :
s.max' H = s.sup' H id
theorem finset.min'_eq_inf' {α : Type u_2} [linear_order α] (s : finset α) (H : s.nonempty) :
s.min' H = s.inf' H id
@[simp]
theorem finset.max'_singleton {α : Type u_2} [linear_order α] (a : α) :
{a}.max' _ = a

{a}.max' _ is a.

theorem finset.min'_lt_max' {α : Type u_2} [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_2} [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_2} [linear_order α] {s t : finset α} (H : s.nonempty) (hst : s t) :
s.max' H t.max' _
theorem finset.min'_subset {α : Type u_2} [linear_order α] {s t : finset α} (H : s.nonempty) (hst : s t) :
t.min' _ s.min' H
theorem finset.max'_insert {α : Type u_2} [linear_order α] (a : α) (s : finset α) (H : s.nonempty) :
theorem finset.min'_insert {α : Type u_2} [linear_order α] (a : α) (s : finset α) (H : s.nonempty) :
theorem finset.lt_max'_of_mem_erase_max' {α : Type u_2} [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_2} [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_2} {β : Type u_3} [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_2} {β : Type u_3} [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.coe_max' {α : Type u_2} [linear_order α] {s : finset α} (hs : s.nonempty) :
(s.max' hs) = s.max
theorem finset.coe_min' {α : Type u_2} [linear_order α] {s : finset α} (hs : s.nonempty) :
(s.min' hs) = s.min
theorem finset.max_mem_image_coe {α : Type u_2} [linear_order α] {s : finset α} (hs : s.nonempty) :
theorem finset.min_mem_image_coe {α : Type u_2} [linear_order α] {s : finset α} (hs : s.nonempty) :
theorem finset.max'_erase_ne_self {α : Type u_2} [linear_order α] {x : α} {s : finset α} (s0 : (s.erase x).nonempty) :
(s.erase x).max' s0 x
theorem finset.min'_erase_ne_self {α : Type u_2} [linear_order α] {x : α} {s : finset α} (s0 : (s.erase x).nonempty) :
(s.erase x).min' s0 x
theorem finset.max_erase_ne_self {α : Type u_2} [linear_order α] {x : α} {s : finset α} :
(s.erase x).max x
theorem finset.min_erase_ne_self {α : Type u_2} [linear_order α] {x : α} {s : finset α} :
(s.erase x).min x
theorem finset.exists_next_right {α : Type u_2} [linear_order α] {x : α} {s : finset α} (h : (y : α) (H : y s), x < y) :
(y : α) (H : y s), x < y (z : α), z s x < z y z
theorem finset.exists_next_left {α : Type u_2} [linear_order α] {x : α} {s : finset α} (h : (y : α) (H : y s), y < x) :
(y : α) (H : y s), y < x (z : α), z s z < x z y
theorem finset.card_le_of_interleaved {α : Type u_2} [linear_order α] {s t : finset α} (h : (x : α), x s (y : α), y s x < y ( (z : α), z s z set.Ioo x y) ( (z : α) (H : z t), x < z z < y)) :
s.card t.card + 1

If finsets s and t are interleaved, then finset.card s ≤ finset.card t + 1.

theorem finset.card_le_diff_of_interleaved {α : Type u_2} [linear_order α] {s t : finset α} (h : (x : α), x s (y : α), y s x < y ( (z : α), z s z set.Ioo x y) ( (z : α) (H : z t), x < z z < y)) :
s.card (t \ s).card + 1

If finsets s and t are interleaved, then finset.card s ≤ finset.card (t \ s) + 1.

theorem finset.induction_on_max {α : Type u_2} [linear_order α] [decidable_eq α] {p : finset α Prop} (s : finset α) (h0 : p ) (step : (a : α) (s : finset α), ( (x : α), x s x < a) p s p (has_insert.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_2} [linear_order α] [decidable_eq α] {p : finset α Prop} (s : finset α) (h0 : p ) (step : (a : α) (s : finset α), ( (x : α), x s a < x) p s p (has_insert.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_2} {ι : Type u_5} [linear_order α] [decidable_eq ι] (f : ι α) {p : finset ι Prop} (s : finset ι) (h0 : p ) (step : (a : ι) (s : finset ι), a s ( (x : ι), x s f x f a) p s p (has_insert.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_2} {ι : Type u_5} [linear_order α] [decidable_eq ι] (f : ι α) {p : finset ι Prop} (s : finset ι) (h0 : p ) (step : (a : ι) (s : finset ι), a s ( (x : ι), x s f a f x) p s p (has_insert.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_2} {β : Type u_3} [linear_order α] (s : finset β) (f : β α) (h : s.nonempty) :
(x : β) (H : x s), (x' : β), x' s f x' f x
theorem finset.exists_min_image {α : Type u_2} {β : Type u_3} [linear_order α] (s : finset β) (f : β α) (h : s.nonempty) :
(x : β) (H : x s), (x' : β), x' s f x f x'
theorem finset.is_glb_iff_is_least {α : Type u_2} [linear_order α] (i : α) (s : finset α) (hs : s.nonempty) :
theorem finset.is_lub_iff_is_greatest {α : Type u_2} [linear_order α] (i : α) (s : finset α) (hs : s.nonempty) :
theorem finset.is_glb_mem {α : Type u_2} [linear_order α] {i : α} (s : finset α) (his : is_glb s i) (hs : s.nonempty) :
i s
theorem finset.is_lub_mem {α : Type u_2} [linear_order α] {i : α} (s : finset α) (his : is_lub s i) (hs : s.nonempty) :
i s
theorem multiset.map_finset_sup {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq α] [decidable_eq β] (s : finset γ) (f : γ multiset β) (g : β α) (hg : function.injective g) :
theorem multiset.count_finset_sup {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [decidable_eq α] (s : finset β) (f : β α) :
s.sup (λ (b : β), {f b}) = finset.image f s
@[simp]
theorem finset.sup_singleton' {α : Type u_2} [decidable_eq α] (s : finset α) :
theorem supr_eq_supr_finset {α : Type u_2} {ι : Type u_5} [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_2} {ι' : Sort u_7} [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_2} {ι : Type u_5} [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_2} {ι' : Sort u_7} [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_2} {ι : Type u_5} (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_2} {ι' : Sort u_7} (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_2} {ι : Type u_5} (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_2} {ι' : Sort u_7} (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_2} {ι : Type u_5} [linear_ordered_semiring α] [order_bot α] {a b : ι α} (s : finset ι) (ha : (i : ι), i s 0 a i) (hb : (i : ι), i s 0 b i) :
s.sup (a * b) s.sup a * s.sup b
theorem finset.mul_inf_le_inf_mul_of_nonneg {α : Type u_2} {ι : Type u_5} [linear_ordered_semiring α] [order_top α] {a b : ι α} (s : finset ι) (ha : (i : ι), i s 0 a i) (hb : (i : ι), i s 0 b i) :
s.inf a * s.inf b s.inf (a * b)
theorem finset.sup'_mul_le_mul_sup'_of_nonneg {α : Type u_2} {ι : Type u_5} [linear_ordered_semiring α] {a b : ι α} (s : finset ι) (H : s.nonempty) (ha : (i : ι), i s 0 a i) (hb : (i : ι), i s 0 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_2} {ι : Type u_5} [linear_ordered_semiring α] {a b : ι α} (s : finset ι) (H : s.nonempty) (ha : (i : ι), i s 0 a i) (hb : (i : ι), i s 0 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_2} {β : Type u_3} [has_Sup β] (f : α β) (s : finset α) :
( (x : α) (H : x s), f x) = (x : α) (H : x s), f x
theorem finset.infi_coe {α : Type u_2} {β : Type u_3} [has_Inf β] (f : α β) (s : finset α) :
( (x : α) (H : x s), f x) = (x : α) (H : x s), f x
theorem finset.supr_singleton {α : Type u_2} {β : Type u_3} [complete_lattice β] (a : α) (s : α β) :
( (x : α) (H : x {a}), s x) = s a
theorem finset.infi_singleton {α : Type u_2} {β : Type u_3} [complete_lattice β] (a : α) (s : α β) :
( (x : α) (H : x {a}), s x) = s a
theorem finset.supr_option_to_finset {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [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_2} {β : Type u_3} [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_2} {β : Type u_3} [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_2} {β : Type u_3} [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
theorem finset.infi_insert {α : Type u_2} {β : Type u_3} [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
theorem finset.supr_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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.infi_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [complete_lattice β] [decidable_eq α] {x : α} {t : finset α} (f : α β) {s : β} (hx : x t) :
( (i : α) (H : i has_insert.insert x t), function.update f x s i) = s (i : α) (H : i t), f i
theorem finset.infi_insert_update {α : Type u_2} {β : Type u_3} [complete_lattice β] [decidable_eq α] {x : α} {t : finset α} (f : α β) {s : β} (hx : x t) :
( (i : α) (H : i has_insert.insert x t), function.update f x s i) = s (i : α) (H : i t), f i
theorem finset.supr_bUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} (s : finset α) (t : α set β) :
( (x : α) (H : x s), t x) = (x : α) (H : x s), t x
theorem finset.set_bInter_coe {α : Type u_2} {β : Type u_3} (s : finset α) (t : α set β) :
( (x : α) (H : x s), t x) = (x : α) (H : x s), t x
theorem finset.set_bUnion_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : α set β) :
( (x : α) (H : x {a}), s x) = s a
theorem finset.set_bInter_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : α set β) :
( (x : α) (H : x {a}), s x) = s a
@[simp]
theorem finset.set_bUnion_preimage_singleton {α : Type u_2} {β : Type u_3} (f : α β) (s : finset β) :
( (y : β) (H : y s), f ⁻¹' {y}) = f ⁻¹' s
theorem finset.set_bUnion_option_to_finset {α : Type u_2} {β : Type u_3} (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_2} {β : Type u_3} (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_2} {β : Type u_3} {s : finset α} {f : α set β} {x : α} (h : x s) :
f x (y : α) (H : y s), f y
theorem finset.set_bUnion_union {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [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_2} {β : Type u_3} [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
theorem finset.set_bInter_insert {α : Type u_2} {β : Type u_3} [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
theorem finset.set_bUnion_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [decidable_eq α] {x : α} {t : finset α} (f : α set β) {s : set β} (hx : x t) :
( (i : α) (H : i has_insert.insert x t), function.update f x s i) = s (i : α) (H : i t), f i
theorem finset.set_bInter_insert_update {α : Type u_2} {β : Type u_3} [decidable_eq α] {x : α} {t : finset α} (f : α set β) {s : set β} (hx : x t) :
( (i : α) (H : i has_insert.insert x t), function.update f x s i) = s (i : α) (H : i t), f i
theorem finset.set_bUnion_bUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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