# Lattice operations on finsets #

### sup #

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

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

Equations
Instances For
theorem Finset.sup_def {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} :
@[simp]
theorem Finset.sup_empty {α : Type u_2} {β : Type u_3} [] [] {f : βα} :
@[simp]
theorem Finset.sup_cons {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {b : β} (h : bs) :
Finset.sup (Finset.cons b s h) f = f b
@[simp]
theorem Finset.sup_insert {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} [] {b : β} :
Finset.sup (insert b s) f = f b
@[simp]
theorem Finset.sup_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (s : ) (f : γβ) (g : βα) :
Finset.sup () g = Finset.sup s (g f)
@[simp]
theorem Finset.sup_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (f : γ β) (g : βα) :
Finset.sup () g = Finset.sup s (g f)
@[simp]
theorem Finset.sup_singleton {α : Type u_2} {β : Type u_3} [] [] {f : βα} {b : β} :
Finset.sup {b} f = f b
theorem Finset.sup_sup {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {g : βα} :
Finset.sup s (f g) =
theorem Finset.sup_congr {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
Finset.sup s₁ f = Finset.sup s₂ g
@[simp]
theorem map_finset_sup {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [] [] [] [] [FunLike F α β] [] (f : F) (s : ) (g : ια) :
f () = Finset.sup s (f g)
@[simp]
theorem Finset.sup_le_iff {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {a : α} :
a bs, f b a
theorem Finset.sup_le {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {a : α} :
(bs, f b a) a

Alias of the reverse direction of Finset.sup_le_iff.

theorem Finset.sup_const_le {α : Type u_2} {β : Type u_3} [] [] {s : } {a : α} :
(Finset.sup s fun (x : β) => a) a
theorem Finset.le_sup {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {b : β} (hb : b s) :
f b
theorem Finset.le_sup_of_le {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {a : α} {b : β} (hb : b s) (h : a f b) :
a
theorem Finset.sup_union {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } {f : βα} [] :
Finset.sup (s₁ s₂) f = Finset.sup s₁ f Finset.sup s₂ f
@[simp]
theorem Finset.sup_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {f : βα} [] (s : ) (t : γ) :
Finset.sup () f = Finset.sup s fun (x : γ) => Finset.sup (t x) f
theorem Finset.sup_const {α : Type u_2} {β : Type u_3} [] [] {s : } (h : s.Nonempty) (c : α) :
(Finset.sup s fun (x : β) => c) = c
@[simp]
theorem Finset.sup_bot {α : Type u_2} {β : Type u_3} [] [] (s : ) :
(Finset.sup s fun (x : β) => ) =
theorem Finset.sup_ite {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {g : βα} (p : βProp) [] :
(Finset.sup s fun (i : β) => if p i then f i else g i) = Finset.sup () f Finset.sup (Finset.filter (fun (i : β) => ¬p i) s) g
theorem Finset.sup_mono_fun {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {g : βα} (h : bs, f b g b) :
theorem Finset.sup_mono {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } {f : βα} (h : s₁ s₂) :
Finset.sup s₁ f Finset.sup s₂ f
theorem Finset.sup_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : ) (f : βγα) :
(Finset.sup s fun (b : β) => Finset.sup t (f b)) = Finset.sup t fun (c : γ) => Finset.sup s fun (b : β) => f b c
@[simp]
theorem Finset.sup_attach {α : Type u_2} {β : Type u_3} [] [] (s : ) (f : βα) :
(Finset.sup () fun (x : { x : β // x s }) => f x) =
theorem Finset.sup_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : ) (f : β × γα) :
Finset.sup (s ×ˢ t) f = Finset.sup s fun (i : β) => Finset.sup t fun (i' : γ) => f (i, i')

See also Finset.product_biUnion.

theorem Finset.sup_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : ) (f : β × γα) :
Finset.sup (s ×ˢ t) f = Finset.sup t fun (i' : γ) => Finset.sup s fun (i : β) => f (i, i')
@[simp]
theorem Finset.sup_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [] [] [] [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
Finset.sup (s ×ˢ t) (Prod.map f g) = (, )
@[simp]
theorem Finset.sup_erase_bot {α : Type u_2} [] [] [] (s : ) :
theorem Finset.sup_sdiff_right {α : Type u_7} {β : Type u_8} (s : ) (f : βα) (a : α) :
(Finset.sup s fun (b : β) => f b \ a) = \ a
theorem Finset.comp_sup_eq_sup_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] {s : } {f : βα} (g : αγ) (g_sup : ∀ (x y : α), g (x y) = g x g y) (bot : g = ) :
g () = Finset.sup s (g f)
theorem Finset.sup_coe {α : Type u_2} {β : Type u_3} [] [] {P : αProp} {Pbot : P } {Psup : ∀ ⦃x y : α⦄, P xP yP (x y)} (t : ) (f : β{ x : α // P x }) :
() = Finset.sup t fun (x : β) => (f x)

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

@[simp]
theorem Finset.sup_toFinset {α : Type u_7} {β : Type u_8} [] (s : ) (f : α) :
= Finset.sup s fun (x : α) => Multiset.toFinset (f x)
theorem List.foldr_sup_eq_sup_toFinset {α : Type u_2} [] [] [] (l : List α) :
List.foldr (fun (x x_1 : α) => x x_1) l = Finset.sup () id
theorem Finset.exists_nat_subset_range (s : ) :
∃ (n : ),
theorem Finset.sup_induction {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {p : αProp} (hb : p ) (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
p ()
theorem Finset.sup_le_of_le_directed {α : Type u_7} [] [] (s : Set α) (hs : ) (hdir : DirectedOn (fun (x x_1 : α) => x x_1) s) (t : ) :
(xt, ∃ y ∈ s, x y)∃ x ∈ s, Finset.sup t id x
theorem Finset.sup_mem {α : Type u_2} [] [] (s : Set α) (w₁ : s) (w₂ : xs, ys, x y s) {ι : Type u_7} (t : ) (p : ια) (h : it, p i s) :
s
@[simp]
theorem Finset.sup_eq_bot_iff {α : Type u_2} {β : Type u_3} [] [] (f : βα) (S : ) :
= sS, f s =
theorem Finset.sup_eq_iSup {α : Type u_2} {β : Type u_3} [] (s : ) (f : αβ) :
= ⨆ a ∈ s, f a
theorem Finset.sup_id_eq_sSup {α : Type u_2} [] (s : ) :
Finset.sup s id = sSup s
theorem Finset.sup_id_set_eq_sUnion {α : Type u_2} (s : Finset (Set α)) :
Finset.sup s id = ⋃₀ s
@[simp]
theorem Finset.sup_set_eq_biUnion {α : Type u_2} {β : Type u_3} (s : ) (f : αSet β) :
= ⋃ x ∈ s, f x
theorem Finset.sup_eq_sSup_image {α : Type u_2} {β : Type u_3} [] (s : ) (f : αβ) :
= sSup (f '' s)

### inf #

def Finset.inf {α : Type u_2} {β : Type u_3} [] [] (s : ) (f : βα) :
α

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

Equations
Instances For
theorem Finset.inf_def {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} :
@[simp]
theorem Finset.inf_empty {α : Type u_2} {β : Type u_3} [] [] {f : βα} :
@[simp]
theorem Finset.inf_cons {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {b : β} (h : bs) :
Finset.inf (Finset.cons b s h) f = f b
@[simp]
theorem Finset.inf_insert {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} [] {b : β} :
Finset.inf (insert b s) f = f b
@[simp]
theorem Finset.inf_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (s : ) (f : γβ) (g : βα) :
Finset.inf () g = Finset.inf s (g f)
@[simp]
theorem Finset.inf_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (f : γ β) (g : βα) :
Finset.inf () g = Finset.inf s (g f)
@[simp]
theorem Finset.inf_singleton {α : Type u_2} {β : Type u_3} [] [] {f : βα} {b : β} :
Finset.inf {b} f = f b
theorem Finset.inf_inf {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {g : βα} :
Finset.inf s (f g) =
theorem Finset.inf_congr {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
Finset.inf s₁ f = Finset.inf s₂ g
@[simp]
theorem map_finset_inf {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [] [] [] [] [FunLike F α β] [] (f : F) (s : ) (g : ια) :
f () = Finset.inf s (f g)
@[simp]
theorem Finset.le_inf_iff {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {a : α} :
a bs, a f b
theorem Finset.le_inf {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {a : α} :
(bs, a f b)a

Alias of the reverse direction of Finset.le_inf_iff.

theorem Finset.le_inf_const_le {α : Type u_2} {β : Type u_3} [] [] {s : } {a : α} :
a Finset.inf s fun (x : β) => a
theorem Finset.inf_le {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {b : β} (hb : b s) :
f b
theorem Finset.inf_le_of_le {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {a : α} {b : β} (hb : b s) (h : f b a) :
a
theorem Finset.inf_union {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } {f : βα} [] :
Finset.inf (s₁ s₂) f = Finset.inf s₁ f Finset.inf s₂ f
@[simp]
theorem Finset.inf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {f : βα} [] (s : ) (t : γ) :
Finset.inf () f = Finset.inf s fun (x : γ) => Finset.inf (t x) f
theorem Finset.inf_const {α : Type u_2} {β : Type u_3} [] [] {s : } (h : s.Nonempty) (c : α) :
(Finset.inf s fun (x : β) => c) = c
@[simp]
theorem Finset.inf_top {α : Type u_2} {β : Type u_3} [] [] (s : ) :
(Finset.inf s fun (x : β) => ) =
theorem Finset.inf_ite {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {g : βα} (p : βProp) [] :
(Finset.inf s fun (i : β) => if p i then f i else g i) = Finset.inf () f Finset.inf (Finset.filter (fun (i : β) => ¬p i) s) g
theorem Finset.inf_mono_fun {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {g : βα} (h : bs, f b g b) :
theorem Finset.inf_mono {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } {f : βα} (h : s₁ s₂) :
Finset.inf s₂ f Finset.inf s₁ f
theorem Finset.inf_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : ) (f : βγα) :
(Finset.inf s fun (b : β) => Finset.inf t (f b)) = Finset.inf t fun (c : γ) => Finset.inf s fun (b : β) => f b c
theorem Finset.inf_attach {α : Type u_2} {β : Type u_3} [] [] (s : ) (f : βα) :
(Finset.inf () fun (x : { x : β // x s }) => f x) =
theorem Finset.inf_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : ) (f : β × γα) :
Finset.inf (s ×ˢ t) f = Finset.inf s fun (i : β) => Finset.inf t fun (i' : γ) => f (i, i')
theorem Finset.inf_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : ) (f : β × γα) :
Finset.inf (s ×ˢ t) f = Finset.inf t fun (i' : γ) => Finset.inf s fun (i : β) => f (i, i')
@[simp]
theorem Finset.inf_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [] [] [] [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
Finset.inf (s ×ˢ t) (Prod.map f g) = (, )
@[simp]
theorem Finset.inf_erase_top {α : Type u_2} [] [] [] (s : ) :
theorem Finset.comp_inf_eq_inf_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] {s : } {f : βα} (g : αγ) (g_inf : ∀ (x y : α), g (x y) = g x g y) (top : g = ) :
g () = Finset.inf s (g f)
theorem Finset.inf_coe {α : Type u_2} {β : Type u_3} [] [] {P : αProp} {Ptop : P } {Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)} (t : ) (f : β{ x : α // P x }) :
() = Finset.inf t fun (x : β) => (f x)

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

theorem List.foldr_inf_eq_inf_toFinset {α : Type u_2} [] [] [] (l : List α) :
List.foldr (fun (x x_1 : α) => x x_1) l = Finset.inf () id
theorem Finset.inf_induction {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {p : αProp} (ht : p ) (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
p ()
theorem Finset.inf_mem {α : Type u_2} [] [] (s : Set α) (w₁ : s) (w₂ : xs, ys, x y s) {ι : Type u_7} (t : ) (p : ια) (h : it, p i s) :
s
@[simp]
theorem Finset.inf_eq_top_iff {α : Type u_2} {β : Type u_3} [] [] (f : βα) (S : ) :
= sS, f s =
@[simp]
theorem Finset.toDual_sup {α : Type u_2} {β : Type u_3} [] [] (s : ) (f : βα) :
OrderDual.toDual () = Finset.inf s (OrderDual.toDual f)
@[simp]
theorem Finset.toDual_inf {α : Type u_2} {β : Type u_3} [] [] (s : ) (f : βα) :
OrderDual.toDual () = Finset.sup s (OrderDual.toDual f)
@[simp]
theorem Finset.ofDual_sup {α : Type u_2} {β : Type u_3} [] [] (s : ) (f : βαᵒᵈ) :
OrderDual.ofDual () = Finset.inf s (OrderDual.ofDual f)
@[simp]
theorem Finset.ofDual_inf {α : Type u_2} {β : Type u_3} [] [] (s : ) (f : βαᵒᵈ) :
OrderDual.ofDual () = Finset.sup s (OrderDual.ofDual f)
theorem Finset.sup_inf_distrib_left {α : Type u_2} {ι : Type u_5} [] [] (s : ) (f : ια) (a : α) :
a = Finset.sup s fun (i : ι) => a f i
theorem Finset.sup_inf_distrib_right {α : Type u_2} {ι : Type u_5} [] [] (s : ) (f : ια) (a : α) :
a = Finset.sup s fun (i : ι) => f i a
theorem Finset.disjoint_sup_right {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} :
Disjoint a () ∀ ⦃i : ι⦄, i sDisjoint a (f i)
theorem Finset.disjoint_sup_left {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} :
Disjoint () a ∀ ⦃i : ι⦄, i sDisjoint (f i) a
theorem Finset.sup_inf_sup {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [] [] (s : ) (t : ) (f : ια) (g : κα) :
= Finset.sup (s ×ˢ t) fun (i : ι × κ) => f i.1 g i.2
theorem Finset.inf_sup_distrib_left {α : Type u_2} {ι : Type u_5} [] [] (s : ) (f : ια) (a : α) :
a = Finset.inf s fun (i : ι) => a f i
theorem Finset.inf_sup_distrib_right {α : Type u_2} {ι : Type u_5} [] [] (s : ) (f : ια) (a : α) :
a = Finset.inf s fun (i : ι) => f i a
theorem Finset.codisjoint_inf_right {α : Type u_2} {ι : Type u_5} [] [] {f : ια} {s : } {a : α} :
Codisjoint a () ∀ ⦃i : ι⦄, i sCodisjoint a (f i)
theorem Finset.codisjoint_inf_left {α : Type u_2} {ι : Type u_5} [] [] {f : ια} {s : } {a : α} :
Codisjoint () a ∀ ⦃i : ι⦄, i sCodisjoint (f i) a
theorem Finset.inf_sup_inf {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [] [] (s : ) (t : ) (f : ια) (g : κα) :
= Finset.inf (s ×ˢ t) fun (i : ι × κ) => f i.1 g i.2
theorem Finset.inf_sup {α : Type u_2} {ι : Type u_5} [] [] [] {κ : ιType u_7} (s : ) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ iα) :
(Finset.inf s fun (i : ι) => Finset.sup (t i) (f i)) = Finset.sup () fun (g : (a : ι) → a sκ a) => Finset.inf () fun (i : { x : ι // x s }) => f (i) (g i )
theorem Finset.sup_inf {α : Type u_2} {ι : Type u_5} [] [] [] {κ : ιType u_7} (s : ) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ iα) :
(Finset.sup s fun (i : ι) => Finset.inf (t i) (f i)) = Finset.inf () fun (g : (a : ι) → a sκ a) => Finset.sup () fun (i : { x : ι // x s }) => f (i) (g i )
theorem Finset.sup_sdiff_left {α : Type u_2} {ι : Type u_5} [] (s : ) (f : ια) (a : α) :
(Finset.sup s fun (b : ι) => a \ f b) = a \
theorem Finset.inf_sdiff_left {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
(Finset.inf s fun (b : ι) => a \ f b) = a \
theorem Finset.inf_sdiff_right {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
(Finset.inf s fun (b : ι) => f b \ a) = \ a
theorem Finset.inf_himp_right {α : Type u_2} {ι : Type u_5} [] (s : ) (f : ια) (a : α) :
(Finset.inf s fun (b : ι) => f b a) = a
theorem Finset.sup_himp_right {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
(Finset.sup s fun (b : ι) => f b a) = a
theorem Finset.sup_himp_left {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
(Finset.sup s fun (b : ι) => a f b) = a
@[simp]
theorem Finset.compl_sup {α : Type u_2} {ι : Type u_5} [] (s : ) (f : ια) :
() = Finset.inf s fun (i : ι) => (f i)
@[simp]
theorem Finset.compl_inf {α : Type u_2} {ι : Type u_5} [] (s : ) (f : ια) :
() = Finset.sup s fun (i : ι) => (f i)
theorem Finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [] [] {s : } {f : ια} [] [] (g : αβ) (mono_g : ) (bot : g = ) :
g () = Finset.sup s (g f)
@[simp]
theorem Finset.le_sup_iff {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} (ha : < a) :
a ∃ b ∈ s, a f b
@[simp]
theorem Finset.lt_sup_iff {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} :
a < ∃ b ∈ s, a < f b
@[simp]
theorem Finset.sup_lt_iff {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} (ha : < a) :
< a bs, f b < a
theorem Finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [] [] {s : } {f : ια} [] [] (g : αβ) (mono_g : ) (top : g = ) :
g () = Finset.inf s (g f)
@[simp]
theorem Finset.inf_le_iff {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} (ha : a < ) :
a ∃ b ∈ s, f b a
@[simp]
theorem Finset.inf_lt_iff {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} :
< a ∃ b ∈ s, f b < a
@[simp]
theorem Finset.lt_inf_iff {α : Type u_2} {ι : Type u_5} [] [] {s : } {f : ια} {a : α} (ha : a < ) :
a < bs, a < f b
theorem Finset.inf_eq_iInf {α : Type u_2} {β : Type u_3} [] (s : ) (f : αβ) :
= ⨅ a ∈ s, f a
theorem Finset.inf_id_eq_sInf {α : Type u_2} [] (s : ) :
Finset.inf s id = sInf s
theorem Finset.inf_id_set_eq_sInter {α : Type u_2} (s : Finset (Set α)) :
Finset.inf s id = ⋂₀ s
@[simp]
theorem Finset.inf_set_eq_iInter {α : Type u_2} {β : Type u_3} (s : ) (f : αSet β) :
= ⋂ x ∈ s, f x
theorem Finset.inf_eq_sInf_image {α : Type u_2} {β : Type u_3} [] (s : ) (f : αβ) :
= sInf (f '' s)
theorem Finset.sup_of_mem {α : Type u_2} {β : Type u_3} [] {s : } (f : βα) {b : β} (h : b s) :
∃ (a : α), Finset.sup s (WithBot.some f) = a
def Finset.sup' {α : Type u_2} {β : Type u_3} [] (s : ) (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
Instances For
@[simp]
theorem Finset.coe_sup' {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) :
(Finset.sup' s H f) = Finset.sup s (WithBot.some f)
@[simp]
theorem Finset.sup'_cons {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {b : β} {hb : bs} :
Finset.sup' (Finset.cons b s hb) f = f b Finset.sup' s H f
@[simp]
theorem Finset.sup'_insert {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) [] {b : β} :
Finset.sup' (insert b s) f = f b Finset.sup' s H f
@[simp]
theorem Finset.sup'_singleton {α : Type u_2} {β : Type u_3} [] (f : βα) {b : β} :
Finset.sup' {b} f = f b
@[simp]
theorem Finset.sup'_le_iff {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {a : α} :
Finset.sup' s H f a bs, f b a
theorem Finset.sup'_le {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {a : α} :
(bs, f b a)Finset.sup' s H f a

Alias of the reverse direction of Finset.sup'_le_iff.

theorem Finset.le_sup' {α : Type u_2} {β : Type u_3} [] {s : } (f : βα) {b : β} (h : b s) :
f b Finset.sup' s f
theorem Finset.le_sup'_of_le {α : Type u_2} {β : Type u_3} [] {s : } (f : βα) {a : α} {b : β} (hb : b s) (h : a f b) :
a Finset.sup' s f
@[simp]
theorem Finset.sup'_const {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (a : α) :
(Finset.sup' s H fun (x : β) => a) = a
theorem Finset.sup'_union {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : βα) :
Finset.sup' (s₁ s₂) f = Finset.sup' s₁ h₁ f Finset.sup' s₂ h₂ f
theorem Finset.sup'_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] (f : βα) [] {s : } (Hs : s.Nonempty) {t : γ} (Ht : ∀ (b : γ), (t b).Nonempty) :
Finset.sup' () f = Finset.sup' s Hs fun (b : γ) => Finset.sup' (t b) f
theorem Finset.sup'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : βγα) :
(Finset.sup' s hs fun (b : β) => Finset.sup' t ht (f b)) = Finset.sup' t ht fun (c : γ) => Finset.sup' s hs fun (b : β) => f b c
theorem Finset.sup'_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {t : } (h : (s ×ˢ t).Nonempty) (f : β × γα) :
Finset.sup' (s ×ˢ t) h f = Finset.sup' s fun (i : β) => Finset.sup' t fun (i' : γ) => f (i, i')
theorem Finset.sup'_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {t : } (h : (s ×ˢ t).Nonempty) (f : β × γα) :
Finset.sup' (s ×ˢ t) h f = Finset.sup' t fun (i' : γ) => Finset.sup' s fun (i : β) => f (i, i')
theorem Finset.prodMk_sup'_sup' {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [] [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
(Finset.sup' s hs f, Finset.sup' t ht g) = Finset.sup' (s ×ˢ t) (Prod.map f g)

See also Finset.sup'_prodMap.

theorem Finset.sup'_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [] [] {s : } {t : } (hst : (s ×ˢ t).Nonempty) (f : ια) (g : κβ) :
Finset.sup' (s ×ˢ t) hst (Prod.map f g) = (Finset.sup' s f, Finset.sup' t g)

See also Finset.prodMk_sup'_sup'.

theorem Finset.sup'_induction {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {p : αProp} (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
p (Finset.sup' s H f)
theorem Finset.sup'_mem {α : Type u_2} [] (s : Set α) (w : xs, ys, x y s) {ι : Type u_7} (t : ) (H : t.Nonempty) (p : ια) (h : it, p i s) :
theorem Finset.sup'_congr {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) {t : } {f : βα} {g : βα} (h₁ : s = t) (h₂ : xs, f x = g x) :
Finset.sup' s H f = Finset.sup' t g
theorem Finset.comp_sup'_eq_sup'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {s : } (H : s.Nonempty) {f : βα} (g : αγ) (g_sup : ∀ (x y : α), g (x y) = g x g y) :
g (Finset.sup' s H f) = Finset.sup' s H (g f)
@[simp]
theorem map_finset_sup' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [] [] [FunLike F α β] [SupHomClass F α β] (f : F) {s : } (hs : s.Nonempty) (g : ια) :
f (Finset.sup' s hs g) = Finset.sup' s hs (f g)
theorem Finset.nsmul_sup' {α : Type u_2} {β : Type u_3} {s : } (hs : s.Nonempty) (f : αβ) (n : ) :
(Finset.sup' s hs fun (a : α) => n f a) = n Finset.sup' s hs f
@[simp]
theorem Finset.sup'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {s : } {f : γβ} (hs : ().Nonempty) (g : βα) :
Finset.sup' () hs g = Finset.sup' s (g f)

To rewrite from right to left, use Finset.sup'_comp_eq_image.

theorem Finset.sup'_comp_eq_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {s : } {f : γβ} (hs : s.Nonempty) (g : βα) :
Finset.sup' s hs (g f) = Finset.sup' () g

A version of Finset.sup'_image with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

@[simp]
theorem Finset.sup'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {f : γ β} (g : βα) (hs : ().Nonempty) :
Finset.sup' () hs g = Finset.sup' s (g f)

To rewrite from right to left, use Finset.sup'_comp_eq_map.

theorem Finset.sup'_comp_eq_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {f : γ β} (g : βα) (hs : s.Nonempty) :
Finset.sup' s hs (g f) = Finset.sup' () g

A version of Finset.sup'_map with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

theorem Finset.sup'_mono {α : Type u_2} {β : Type u_3} [] (f : βα) {s₁ : } {s₂ : } (h : s₁ s₂) (h₁ : s₁.Nonempty) :
Finset.sup' s₁ h₁ f Finset.sup' s₂ f
theorem GCongr.finset_sup'_le {α : Type u_2} {β : Type u_3} [] (f : βα) {s₁ : } {s₂ : } (h : s₁ s₂) {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} :
Finset.sup' s₁ h₁ f Finset.sup' s₂ h₂ f

A version of Finset.sup'_mono acceptable for @[gcongr]. Instead of deducing s₂.Nonempty from s₁.Nonempty and s₁ ⊆ s₂, this version takes it as an argument.

theorem Finset.inf_of_mem {α : Type u_2} {β : Type u_3} [] {s : } (f : βα) {b : β} (h : b s) :
∃ (a : α), Finset.inf s (WithTop.some f) = a
def Finset.inf' {α : Type u_2} {β : Type u_3} [] (s : ) (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
Instances For
@[simp]
theorem Finset.coe_inf' {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) :
(Finset.inf' s H f) = Finset.inf s (WithTop.some f)
@[simp]
theorem Finset.inf'_cons {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {b : β} {hb : bs} :
Finset.inf' (Finset.cons b s hb) f = f b Finset.inf' s H f
@[simp]
theorem Finset.inf'_insert {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) [] {b : β} :
Finset.inf' (insert b s) f = f b Finset.inf' s H f
@[simp]
theorem Finset.inf'_singleton {α : Type u_2} {β : Type u_3} [] (f : βα) {b : β} :
Finset.inf' {b} f = f b
@[simp]
theorem Finset.le_inf'_iff {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {a : α} :
a Finset.inf' s H f bs, a f b
theorem Finset.le_inf' {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {a : α} (hs : bs, a f b) :
theorem Finset.inf'_le {α : Type u_2} {β : Type u_3} [] {s : } (f : βα) {b : β} (h : b s) :
Finset.inf' s f f b
theorem Finset.inf'_le_of_le {α : Type u_2} {β : Type u_3} [] {s : } (f : βα) {a : α} {b : β} (hb : b s) (h : f b a) :
Finset.inf' s f a
@[simp]
theorem Finset.inf'_const {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (a : α) :
(Finset.inf' s H fun (x : β) => a) = a
theorem Finset.inf'_union {α : Type u_2} {β : Type u_3} [] [] {s₁ : } {s₂ : } (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : βα) :
Finset.inf' (s₁ s₂) f = Finset.inf' s₁ h₁ f Finset.inf' s₂ h₂ f
theorem Finset.inf'_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] (f : βα) [] {s : } (Hs : s.Nonempty) {t : γ} (Ht : ∀ (b : γ), (t b).Nonempty) :
Finset.inf' () f = Finset.inf' s Hs fun (b : γ) => Finset.inf' (t b) f
theorem Finset.inf'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : βγα) :
(Finset.inf' s hs fun (b : β) => Finset.inf' t ht (f b)) = Finset.inf' t ht fun (c : γ) => Finset.inf' s hs fun (b : β) => f b c
theorem Finset.inf'_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {t : } (h : (s ×ˢ t).Nonempty) (f : β × γα) :
Finset.inf' (s ×ˢ t) h f = Finset.inf' s fun (i : β) => Finset.inf' t fun (i' : γ) => f (i, i')
theorem Finset.inf'_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {t : } (h : (s ×ˢ t).Nonempty) (f : β × γα) :
Finset.inf' (s ×ˢ t) h f = Finset.inf' t fun (i' : γ) => Finset.inf' s fun (i : β) => f (i, i')
theorem Finset.prodMk_inf'_inf' {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [] [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
(Finset.inf' s hs f, Finset.inf' t ht g) = Finset.inf' (s ×ˢ t) (Prod.map f g)

See also Finset.inf'_prodMap.

theorem Finset.inf'_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [] [] {s : } {t : } (hst : (s ×ˢ t).Nonempty) (f : ια) (g : κβ) :
Finset.inf' (s ×ˢ t) hst (Prod.map f g) = (Finset.inf' s f, Finset.inf' t g)

See also Finset.prodMk_inf'_inf'.

theorem Finset.comp_inf'_eq_inf'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {s : } (H : s.Nonempty) {f : βα} (g : αγ) (g_inf : ∀ (x y : α), g (x y) = g x g y) :
g (Finset.inf' s H f) = Finset.inf' s H (g f)
theorem Finset.inf'_induction {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) (f : βα) {p : αProp} (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
p (Finset.inf' s H f)
theorem Finset.inf'_mem {α : Type u_2} [] (s : Set α) (w : xs, ys, x y s) {ι : Type u_7} (t : ) (H : t.Nonempty) (p : ια) (h : it, p i s) :
theorem Finset.inf'_congr {α : Type u_2} {β : Type u_3} [] {s : } (H : s.Nonempty) {t : } {f : βα} {g : βα} (h₁ : s = t) (h₂ : xs, f x = g x) :
Finset.inf' s H f = Finset.inf' t g
@[simp]
theorem map_finset_inf' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [] [] [FunLike F α β] [InfHomClass F α β] (f : F) {s : } (hs : s.Nonempty) (g : ια) :
f (Finset.inf' s hs g) = Finset.inf' s hs (f g)
theorem Finset.nsmul_inf' {α : Type u_2} {β : Type u_3} {s : } (hs : s.Nonempty) (f : αβ) (n : ) :
(Finset.inf' s hs fun (a : α) => n f a) = n Finset.inf' s hs f
@[simp]
theorem Finset.inf'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {s : } {f : γβ} (hs : ().Nonempty) (g : βα) :
Finset.inf' () hs g = Finset.inf' s (g f)

To rewrite from right to left, use Finset.inf'_comp_eq_image.

theorem Finset.inf'_comp_eq_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {s : } {f : γβ} (hs : s.Nonempty) (g : βα) :
Finset.inf' s hs (g f) = Finset.inf' () g

A version of Finset.inf'_image with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

@[simp]
theorem Finset.inf'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {f : γ β} (g : βα) (hs : ().Nonempty) :
Finset.inf' () hs g = Finset.inf' s (g f)

To rewrite from right to left, use Finset.inf'_comp_eq_map.

theorem Finset.inf'_comp_eq_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {s : } {f : γ β} (g : βα) (hs : s.Nonempty) :
Finset.inf' s hs (g f) = Finset.inf' () g

A version of Finset.inf'_map with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

theorem Finset.inf'_mono {α : Type u_2} {β : Type u_3} [] (f : βα) {s₁ : } {s₂ : } (h : s₁ s₂) (h₁ : s₁.Nonempty) :
Finset.inf' s₂ f Finset.inf' s₁ h₁ f
theorem GCongr.finset_inf'_mono {α : Type u_2} {β : Type u_3} [] (f : βα) {s₁ : } {s₂ : } (h : s₁ s₂) {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} :
Finset.inf' s₂ h₂ f Finset.inf' s₁ h₁ f

A version of Finset.inf'_mono acceptable for @[gcongr]. Instead of deducing s₂.Nonempty from s₁.Nonempty and s₁ ⊆ s₂, this version takes it as an argument.

theorem Finset.sup'_eq_sup {α : Type u_2} {β : Type u_3} [] [] {s : } (H : s.Nonempty) (f : βα) :
Finset.sup' s H f =
theorem Finset.coe_sup_of_nonempty {α : Type u_2} {β : Type u_3} [] [] {s : } (h : s.Nonempty) (f : βα) :
() = Finset.sup s (WithBot.some f)
theorem Finset.inf'_eq_inf {α : Type u_2} {β : Type u_3} [] [] {s : } (H : s.Nonempty) (f : βα) :
Finset.inf' s H f =
theorem Finset.coe_inf_of_nonempty {α : Type u_2} {β : Type u_3} [] [] {s : } (h : s.Nonempty) (f : βα) :
() = Finset.inf s (WithTop.some f)
@[simp]
theorem Finset.sup_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeSup (C b)] [(b : β) → OrderBot (C b)] (s : ) (f : α(b : β) → C b) (b : β) :
Finset.sup s f b = Finset.sup s fun (a : α) => f a b
@[simp]
theorem Finset.inf_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeInf (C b)] [(b : β) → OrderTop (C b)] (s : ) (f : α(b : β) → C b) (b : β) :
Finset.inf s f b = Finset.inf s fun (a : α) => f a b
@[simp]
theorem Finset.sup'_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeSup (C b)] {s : } (H : s.Nonempty) (f : α(b : β) → C b) (b : β) :
Finset.sup' s H f b = Finset.sup' s H fun (a : α) => f a b
@[simp]
theorem Finset.inf'_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeInf (C b)] {s : } (H : s.Nonempty) (f : α(b : β) → C b) (b : β) :
Finset.inf' s H f b = Finset.inf' s H fun (a : α) => f a b
@[simp]
theorem Finset.toDual_sup' {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) :
OrderDual.toDual (Finset.sup' s hs f) = Finset.inf' s hs (OrderDual.toDual f)
@[simp]
theorem Finset.toDual_inf' {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) :
OrderDual.toDual (Finset.inf' s hs f) = Finset.sup' s hs (OrderDual.toDual f)
@[simp]
theorem Finset.ofDual_sup' {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ιαᵒᵈ) :
OrderDual.ofDual (Finset.sup' s hs f) = Finset.inf' s hs (OrderDual.ofDual f)
@[simp]
theorem Finset.ofDual_inf' {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ιαᵒᵈ) :
OrderDual.ofDual (Finset.inf' s hs f) = Finset.sup' s hs (OrderDual.ofDual f)
theorem Finset.sup'_inf_distrib_left {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
a Finset.sup' s hs f = Finset.sup' s hs fun (i : ι) => a f i
theorem Finset.sup'_inf_distrib_right {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
Finset.sup' s hs f a = Finset.sup' s hs fun (i : ι) => f i a
theorem Finset.sup'_inf_sup' {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κα) :
Finset.sup' s hs f Finset.sup' t ht g = Finset.sup' (s ×ˢ t) fun (i : ι × κ) => f i.1 g i.2
theorem Finset.inf'_sup_distrib_left {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
a Finset.inf' s hs f = Finset.inf' s hs fun (i : ι) => a f i
theorem Finset.inf'_sup_distrib_right {α : Type u_2} {ι : Type u_5} [] {s : } (hs : s.Nonempty) (f : ια) (a : α) :
Finset.inf' s hs f a = Finset.inf' s hs fun (i : ι) => f i a
theorem Finset.inf'_sup_inf' {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κα) :
Finset.inf' s hs f Finset.inf' t ht g = Finset.inf' (s ×ˢ t) fun (i : ι × κ) => f i.1 g i.2
@[simp]
theorem Finset.le_sup'_iff {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) {f : ια} {a : α} :
a Finset.sup' s H f ∃ b ∈ s, a f b
@[simp]
theorem Finset.lt_sup'_iff {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) {f : ια} {a : α} :
a < Finset.sup' s H f ∃ b ∈ s, a < f b
@[simp]
theorem Finset.sup'_lt_iff {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) {f : ια} {a : α} :
Finset.sup' s H f < a is, f i < a
@[simp]
theorem Finset.inf'_le_iff {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) {f : ια} {a : α} :
Finset.inf' s H f a ∃ i ∈ s, f i a
@[simp]
theorem Finset.inf'_lt_iff {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) {f : ια} {a : α} :
Finset.inf' s H f < a ∃ i ∈ s, f i < a
@[simp]
theorem Finset.lt_inf'_iff {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) {f : ια} {a : α} :
a < Finset.inf' s H f is, a < f i
theorem Finset.exists_mem_eq_sup' {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) (f : ια) :
∃ i ∈ s, Finset.sup' s H f = f i
theorem Finset.exists_mem_eq_inf' {α : Type u_2} {ι : Type u_5} [] {s : } (H : s.Nonempty) (f : ια) :
∃ i ∈ s, Finset.inf' s H f = f i
theorem Finset.exists_mem_eq_sup {α : Type u_2} {ι : Type u_5} [] [] (s : ) (h : s.Nonempty) (f : ια) :
∃ i ∈ s, = f i
theorem Finset.exists_mem_eq_inf {α : Type u_2} {ι : Type u_5} [] [] (s : ) (h : s.Nonempty) (f : ια) :
∃ i ∈ s, = f i

### max and min of finite sets #

def Finset.max {α : Type u_2} [] (s : ) :

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 WithBot α. If you want to get an element of α, see s.max'.

Equations
Instances For
theorem Finset.max_eq_sup_coe {α : Type u_2} [] {s : } :
= Finset.sup s WithBot.some
theorem Finset.max_eq_sup_withBot {α : Type u_2} [] (s : ) :
= Finset.sup s WithBot.some
@[simp]
theorem Finset.max_empty {α : Type u_2} [] :
@[simp]
theorem Finset.max_insert {α : Type u_2} [] {a : α} {s : } :
Finset.max (insert a s) = max (a) ()
@[simp]
theorem Finset.max_singleton {α : Type u_2} [] {a : α} :
Finset.max {a} = a
theorem Finset.max_of_mem {α : Type u_2} [] {s : } {a : α} (h : a s) :
∃ (b : α), = b
theorem Finset.max_of_nonempty {α : Type u_2} [] {s : } (h : s.Nonempty) :
∃ (a : α), = a
theorem Finset.max_eq_bot {α : Type u_2} [] {s : } :
s =
theorem Finset.mem_of_max {α : Type u_2} [] {s : } {a : α} :
= aa s
theorem Finset.le_max {α : Type u_2} [] {a : α} {s : } (as : a s) :
a
theorem Finset.not_mem_of_max_lt_coe {α : Type u_2} [] {a : α} {s : } (h : < a) :
as
theorem Finset.le_max_of_eq {α : Type u_2} [] {s : } {a : α} {b : α} (h₁ : a s) (h₂ : = b) :
a b
theorem Finset.not_mem_of_max_lt {α : Type u_2} [] {s : } {a : α} {b : α} (h₁ : b < a) (h₂ : = b) :
as
theorem Finset.max_mono {α : Type u_2} [] {s : } {t : } (st : s t) :
theorem Finset.max_le {α : Type u_2} [] {M : } {s : } (st : as, a M) :
M
def Finset.min {α : Type u_2} [] (s : ) :

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 WithTop α. If you want to get an element of α, see s.min'.

Equations
Instances For
theorem Finset.min_eq_inf_withTop {α : Type u_2} [] (s : ) :
= Finset.inf s WithTop.some
@[simp]
theorem Finset.min_empty {α : Type u_2} [] :
@[simp]
theorem Finset.min_insert {α : Type u_2} [] {a : α} {s : } :
Finset.min (insert a s) = min (a) ()
@[simp]
theorem Finset.min_singleton {α : Type u_2} [] {a : α} :
Finset.min {a} = a
theorem Finset.min_of_mem {α : Type u_2} [] {s : } {a : α} (h : a s) :
∃ (b : α), = b
theorem Finset.min_of_nonempty {α : Type u_2} [] {s : } (h : s.Nonempty) :
∃ (a : α), = a
theorem Finset.min_eq_top {α : Type u_2} [] {s : } :
s =
theorem Finset.mem_of_min {α : Type u_2} [] {s : } {a : α} :
= aa s
theorem Finset.min_le {α : Type u_2} [] {a : α} {s : } (as : a s) :
a
theorem Finset.not_mem_of_coe_lt_min {α : Type u_2} [] {a : α} {s : } (h : a < ) :
as
theorem Finset.min_le_of_eq {α : Type u_2} [] {s : } {a : α} {b : α} (h₁ : b s) (h₂ : = a) :
a b
theorem Finset.not_mem_of_lt_min {α : Type u_2} [] {s : } {a : α} {b : α} (h₁ : a < b) (h₂ : = b) :
as
theorem Finset.min_mono {α : Type u_2} [] {s : } {t : } (st : s t) :
theorem Finset.le_min {α : Type u_2} [] {m : } {s : } (st : as, m a) :
m
def Finset.min' {α : Type u_2} [] (s : ) (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 WithTop α.

Equations
Instances For
def Finset.max' {α : Type u_2} [] (s : ) (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 WithBot α.

Equations
Instances For
theorem Finset.min'_mem {α : Type u_2} [] (s : ) (H : s.Nonempty) :
s
theorem Finset.min'_le {α : Type u_2} [] (s : ) (x : α) (H2 : x s) :
x
theorem Finset.le_min' {α : Type u_2} [] (s : ) (H : s.Nonempty) (x : α) (H2 : ys, x y) :
x
theorem Finset.isLeast_min' {α : Type u_2} [] (s : ) (H : s.Nonempty) :
IsLeast (s) ()
@[simp]
theorem Finset.le_min'_iff {α : Type u_2} [] (s : ) (H : s.Nonempty) {x : α} :
x ys, x y
@[simp]
theorem Finset.min'_singleton {α : Type u_2} [] (a : α) :
Finset.min' {a} = a

{a}.min' _ is a.

theorem Finset.max'_mem {α : Type u_2} [] (s : ) (H : s.Nonempty) :
s
theorem Finset.le_max' {α : Type u_2} [] (s : ) (x : α) (H2 : x s) :
x
theorem Finset.max'_le {α : Type u_2} [] (s : ) (H : s.Nonempty) (x : α) (H2 : ys, y x) :
x
theorem Finset.isGreatest_max' {α : Type u_2} [] (s : ) (H : s.Nonempty) :
IsGreatest (s) ()
@[simp]
theorem Finset.max'_le_iff {α : Type u_2} [] (s : ) (H : s.Nonempty) {x : α} :
x ys, y x
@[simp]
theorem Finset.max'_lt_iff {α : Type u_2} [] (s : ) (H : s.Nonempty) {x : α} :
< x ys, y < x
@[simp]
theorem Finset.lt_min'_iff {α : Type u_2} [] (s : ) (H : s.Nonempty) {x : α} :
x < ys, x < y
theorem Finset.max'_eq_sup' {α : Type u_2} [] (s : ) (H : s.Nonempty) :
= Finset.sup' s H id
theorem Finset.min'_eq_inf' {α : Type u_2} [] (s : ) (H : s.Nonempty) :
= Finset.inf' s H id
@[simp]
theorem Finset.max'_singleton {α : Type u_2} [] (a : α) :
Finset.max' {a} = a

{a}.max' _ is a.

theorem Finset.min'_lt_max' {α : Type u_2} [] (s : ) {i : α} {j : α} (H1 : i s) (H2 : j s) (H3 : i j) :
<
theorem Finset.min'_lt_max'_of_card {α : Type u_2} [] (s : ) (h₂ : 1 < s.card) :
<

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.map_ofDual_min {α : Type u_2} [] (s : ) :
WithTop.map (OrderDual.ofDual) () = Finset.max (Finset.image (OrderDual.ofDual) s)
theorem Finset.map_ofDual_max {α : Type u_2} [] (s : ) :
WithBot.map (OrderDual.ofDual) () = Finset.min (Finset.image (OrderDual.ofDual) s)
theorem Finset.map_toDual_min {α : Type u_2} [] (s : ) :
WithTop.map (OrderDual.toDual) () = Finset.max (Finset.image (OrderDual.toDual) s)
theorem Finset.map_toDual_max {α : Type u_2} [] (s : ) :
WithBot.map (OrderDual.toDual) () = Finset.min (Finset.image (OrderDual.toDual) s)
theorem Finset.ofDual_min' {α : Type u_2} [] {s : } (hs : s.Nonempty) :
OrderDual.ofDual (Finset.min' s hs) = Finset.max' (Finset.image (OrderDual.ofDual) s)
theorem Finset.ofDual_max' {α : Type u_2} [] {s : } (hs : s.Nonempty) :
OrderDual.ofDual (Finset.max' s hs) = Finset.min' (Finset.image (OrderDual.ofDual) s)
theorem Finset.toDual_min' {α : Type u_2} [] {s : } (hs : s.Nonempty) :
OrderDual.toDual (Finset.min' s hs) = Finset.max' (Finset.image (OrderDual.toDual) s)
theorem Finset.toDual_max' {α : Type u_2} [] {s : } (hs : s.Nonempty) :
OrderDual.toDual (Finset.max' s hs) = Finset.min' (Finset.image (OrderDual.toDual) s)
theorem Finset.max'_subset {α : Type u_2} [] {s : } {t : } (H : s.Nonempty) (hst : s t) :
theorem Finset.min'_subset {α : Type u_2} [] {s : } {t : } (H : s.Nonempty) (hst : s t) :
theorem Finset.max'_insert {α : Type u_2} [] (a : α) (s : ) (H : s.Nonempty) :
Finset.max' (insert a s) = max () a
theorem Finset.min'_insert {α : Type u_2} [] (a : α) (s : ) (H : s.Nonempty) :
Finset.min' (insert a s) = min () a
theorem Finset.lt_max'_of_mem_erase_max' {α : Type u_2} [] (s : ) (H : s.Nonempty) [] {a : α} (ha : a Finset.erase s ()) :
a <
theorem Finset.min'_lt_of_mem_erase_min' {α : Type u_2} [] (s : ) (H : s.Nonempty) [] {a : α} (ha : a Finset.erase s ()) :
< a
@[simp]
theorem Finset.max'_image {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (hf : ) (s : ) (h : ().Nonempty) :
Finset.max' () h = f ()

To rewrite from right to left, use Monotone.map_finset_max'.

theorem Monotone.map_finset_max' {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (hf : ) {s : } (h : s.Nonempty) :
f () = Finset.max' ()

A version of Finset.max'_image with LHS and RHS reversed. Also, this version assumes that s is nonempty, not its image.

@[simp]
theorem Finset.min'_image {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (hf : ) (s : ) (h : ().Nonempty) :
Finset.min' () h = f ()

To rewrite from right to left, use Monotone.map_finset_min'.

theorem Monotone.map_finset_min' {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (hf : ) {s : } (h : s.Nonempty) :
f () = Finset.min' ()

A version of Finset.min'_image with LHS and RHS reversed. Also, this version assumes that s is nonempty, not its image.

theorem Finset.coe_max' {α : Type u_2} [] {s : } (hs : s.Nonempty) :
(Finset.max' s hs) =
theorem Finset.coe_min' {α : Type u_2} [] {s : } (hs : s.Nonempty) :
(Finset.min' s hs) =
theorem Finset.max_mem_image_coe {α : Type u_2} [] {s : } (hs : s.Nonempty) :
Finset.image WithBot.some s
theorem Finset.min_mem_image_coe {α : Type u_2} [] {s : } (hs : s.Nonempty) :
Finset.image WithTop.some s
theorem Finset.max_mem_insert_bot_image_coe {α : Type u_2} [] (s : ) :
insert (Finset.image WithBot.some s)
theorem Finset.min_mem_insert_top_image_coe {α : Type u_2} [] (s : ) :
insert (Finset.image WithTop.some s)
theorem Finset.max'_erase_ne_self {α : Type u_2} [] {x : α} {s : } (s0 : ().Nonempty) :
theorem Finset.min'_erase_ne_self {α : Type u_2} [] {x : α} {s : } (s0 : ().Nonempty) :
theorem Finset.max_erase_ne_self {α : Type u_2} [] {x : α} {s : } :
Finset.max () x
theorem Finset.min_erase_ne_self {α : Type u_2} [] {x : α} {s : } :
Finset.min () x
theorem Finset.exists_next_right {α : Type u_2} [] {x : α} {s : } (h : ∃ y ∈ s, x < y) :
∃ y ∈ s, x < y zs, x < zy z
theorem Finset.exists_next_left {α : Type u_2} [] {x : α} {s : } (h : ∃ y ∈ s, y < x) :
∃ y ∈ s, y < x zs, z < xz y
theorem Finset.card_le_of_interleaved {α : Type u_2} [] {s : } {t : } (h : xs, ys, x < y(zs, zSet.Ioo x y)∃ 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} [] {s : } {t : } (h : xs, ys, x < y(zs, zSet.Ioo x y)∃ 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} [] [] {p : Prop} (s : ) (h0 : p ) (step : ∀ (a : α) (s : ), (xs, x < 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_2} [] [] {p : Prop} (s : ) (h0 : p ) (step : ∀ (a : α) (s : ), (xs, a < 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_2} {ι : Type u_5} [] [] (f : ια) {p : Prop} (s : ) (h0 : p ) (step : ∀ (a : ι) (s : ), as(xs, f 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_2} {ι : Type u_5} [] [] (f : ια) {p : Prop} (s : ) (h0 : p ) (step : ∀ (a : ι) (s : ), as(xs, f 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_2} {β : Type u_3} [] (s : ) (f : βα) (h : s.Nonempty) :
∃ x ∈ s, x's, f x' f x
theorem Finset.exists_min_image {α : Type u_2} {β : Type u_3} [] (s : ) (f : βα) (h : s.Nonempty) :
∃ x ∈ s, x's, f x f x'
theorem Finset.isGLB_iff_isLeast {α : Type u_2} [] (i : α) (s : ) (hs : s.Nonempty) :
IsGLB (s) i IsLeast (s) i
theorem Finset.isLUB_iff_isGreatest {α : Type u_2} [] (i : α) (s : ) (hs : s.Nonempty) :
IsLUB (s) i IsGreatest (s) i
theorem Finset.isGLB_mem {α : Type u_2} [] {i : α} (s : ) (his : IsGLB (s) i) (hs : s.Nonempty) :
i s
theorem Finset.isLUB_mem {α : Type u_2} [] {i : α} (s : ) (his : IsLUB (s) i) (hs : s.Nonempty) :
i s
theorem Multiset.map_finset_sup {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (f : γ) (g : βα) (hg : ) :
theorem Multiset.count_finset_sup {α : Type u_2} {β : Type u_3} [] (s : ) (f : α) (b : β) :
Multiset.count b () = Finset.sup s fun (a : α) => Multiset.count b (f a)
theorem Multiset.mem_sup {α : Type u_7} {β : Type u_8} [] {s : } {f : α} {x : β} :
x ∃ v ∈ s, x f v
theorem Finset.mem_sup {α : Type u_7} {β : Type u_8} [] {s : } {f : α} {x : β} :
x ∃ v ∈ s, x f v
theorem Finset.sup_eq_biUnion {α : Type u_7} {β : Type u_8} [] (s : ) (t : α) :
=
@[simp]
theorem Finset.sup_singleton'' {α : Type u_2} {β : Type u_3} [] (s : ) (f : βα) :
(Finset.sup s fun (b : β) => {f b}) =
@[simp]
theorem Finset.sup_singleton' {α : Type u_2} [] (s : ) :
Finset.sup s singleton = s
theorem iSup_eq_iSup_finset {α : Type u_2} {ι : Type u_5} [] (s : ια) :
⨆ (i : ι), s i = ⨆ (t : ), ⨆ 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 iSup_eq_iSup_finset' for a version that works for ι : Sort*.

theorem iSup_eq_iSup_finset' {α : Type u_2} {ι' : Sort u_7} [] (s : ι'α) :
⨆ (i : ι'), s i = ⨆ (t : Finset (PLift ι')), ⨆ 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 iSup_eq_iSup_finset for a version that assumes ι : Type* but has no PLifts.

theorem iInf_eq_iInf_finset {α : Type u_2} {ι : Type u_5} [] (s : ια) :
⨅ (i : ι), s i = ⨅ (t : ), ⨅ 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 iInf_eq_iInf_finset' for a version that works for ι : Sort*.

theorem iInf_eq_iInf_finset' {α : Type u_2} {ι' : Sort u_7} [] (s : ι'α) :
⨅ (i : ι'), s i = ⨅ (t : Finset (PLift ι')), ⨅ 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 iInf_eq_iInf_finset for a version that assumes ι : Type* but has no PLifts.

theorem Set.iUnion_eq_iUnion_finset {α : Type u_2} {ι : Type u_5} (s : ιSet α) :
⋃ (i : ι), s i = ⋃ (t : ), ⋃ 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 iUnion_eq_iUnion_finset' for a version that works for ι : Sort*.

theorem Set.iUnion_eq_iUnion_finset' {α : Type u_2} {ι' : Sort u_7} (s : ι'Set α) :
⋃ (i : ι'), s i = ⋃ (t : Finset (PLift ι')), ⋃ 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 iUnion_eq_iUnion_finset for a version that assumes ι : Type* but avoids PLifts in the right hand side.

theorem Set.iInter_eq_iInter_finset {α : Type u_2} {ι : Type u_5} (s : ιSet α) :
⋂ (i : ι), s i = ⋂ (t : ), ⋂ 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 iInter_eq_iInter_finset' for a version that works for ι : Sort*.

theorem Set.iInter_eq_iInter_finset' {α : Type u_2} {ι' : Sort u_7} (s : ι'Set α) :
⋂ (i : ι'), s i = ⋂ (t : Finset (PLift ι')), ⋂ 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 iInter_eq_iInter_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} [] {a : ια} {b : ια} (s : ) (ha : is, 0 a i) (hb : is, 0 b i) :
Finset.sup s (a * b) *
theorem Finset.mul_inf_le_inf_mul_of_nonneg {α : Type u_2} {ι : Type u_5} [] {a : ια} {b : ια} (s : ) (ha : is, 0 a i) (hb : is, 0 b i) :
* Finset.inf s (a * b)
theorem Finset.sup'_mul_le_mul_sup'_of_nonneg {α : Type u_2} {ι : Type u_5} {a : ια} {b : ια} (s : ) (H : s.Nonempty) (ha : is, 0 a i) (hb : is, 0 b i) :
Finset.sup' s H (a * b) Finset.sup' s H a * Finset.sup' s H b
theorem Finset.inf'_mul_le_mul_inf'_of_nonneg {α : Type u_2} {ι : Type u_5} {a : ια} {b : ια} (s : ) (H : s.Nonempty) (ha : is, 0 a i) (hb : is, 0 b i) :
Finset.inf' s H a * Finset.inf' s H b Finset.inf' s H (a * b)

### Interaction with big lattice/set operations #

theorem Finset.iSup_coe {α : Type u_2} {β : Type u_3} [] (f : αβ) (s : ) :
⨆ x ∈ s, f x = ⨆ x ∈ s, f x
theorem Finset.iInf_coe {α : Type u_2} {β : Type u_3} [] (f : αβ) (s : ) :
⨅ x ∈ s, f x = ⨅ x ∈ s, f x
theorem Finset.iSup_singleton {α : Type u_2} {β : Type u_3} [] (a : α) (s : αβ) :
⨆ x ∈ {a}, s x = s a
theorem Finset.iInf_singleton {α : Type u_2} {β : Type u_3} [] (a : α) (s : αβ) :
⨅ x ∈ {a}, s x = s a
theorem Finset.iSup_option_toFinset {α : Type u_2} {β : Type u_3} [] (o : ) (f : αβ) :
⨆ x ∈ , f x = ⨆ x ∈ o, f x
theorem Finset.iInf_option_toFinset {α : Type u_2} {β : Type u_3} [] (o : ) (f : αβ) :
⨅ x ∈ , f x = ⨅ x ∈ o, f x
theorem Finset.iSup_union {α : Type u_2} {β : Type u_3} [] [] {f : αβ} {s : } {t : } :
⨆ x ∈ s t, f x = (⨆ x ∈ s, f x) ⨆ x ∈ t, f x
theorem Finset.iInf_union {α : Type u_2} {β : Type u_3} [] [] {f : αβ} {s : } {t : } :
⨅ x ∈ s t, f x = (⨅ x ∈ s, f x) ⨅ x ∈ t, f x
theorem Finset.iSup_insert {α : Type u_2} {β : Type u_3} [] [] (a : α) (s : ) (t : αβ) :
⨆ x ∈ insert a s, t x = t a ⨆ x ∈ s, t x
theorem Finset.iInf_insert {α : Type u_2} {β : Type u_3} [] [] (a : α) (s : ) (t : αβ) :
⨅ x ∈ insert a s, t x = t a ⨅ x ∈ s, t x
theorem Finset.iSup_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {f : γα} {g : αβ} {s : } :
⨆ x ∈ , g x = ⨆ y ∈ s, g (f y)
theorem Finset.iInf_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] {f : γα} {g : αβ} {s : } :
⨅ x ∈ , g x = ⨅ y ∈ s, g (f y)
theorem Finset.iSup_insert_update {α : Type u_2} {β : Type u_3} [] [] {x : α} {t : } (f : αβ) {s : β} (hx : xt) :
⨆ i ∈ insert x t, Function.update f x s i = s ⨆ i ∈ t, f i
theorem Finset.iInf_insert_update {α : Type u_2} {β : Type u_3} [] [] {x : α} {t : } (f : αβ) {s : β} (hx : xt) :
⨅ i ∈ insert x t, Function.update f x s i = s ⨅ i ∈ t, f i
theorem Finset.iSup_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : γ) (f : αβ) :
⨆ y ∈ , f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y
theorem Finset.iInf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] (s : ) (t : γ) (f : αβ) :
⨅ y ∈ , f y = ⨅ x ∈ s, ⨅ y ∈ t x, f y
theorem Finset.set_biUnion_coe {α : Type u_2} {β : Type u_3} (s : ) (t : αSet β) :
⋃ x ∈ s, t x = ⋃ x ∈ s, t x
theorem Finset.set_biInter_coe {α : Type u_2} {β : Type u_3} (s : ) (t : αSet β) :
⋂ x ∈ s, t x = ⋂ x ∈ s, t x
theorem Finset.set_biUnion_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : αSet β) :
⋃ x ∈ {a}, s x = s a
theorem Finset.set_biInter_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : αSet β) :
⋂ x ∈ {a}, s x = s a
@[simp]
theorem Finset.set_biUnion_preimage_singleton {α : Type u_2} {β : Type u_3} (f : αβ) (s : ) :
⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s
theorem Finset.set_biUnion_option_toFinset {α : Type u_2} {β : Type u_3} (o : ) (f : αSet β) :
⋃ x ∈ , f x = ⋃ x ∈ o, f x
theorem Finset.set_biInter_option_toFinset {α : Type u_2} {β : Type u_3} (o : ) (f : αSet β) :
⋂ x ∈ , f x = ⋂ x ∈ o, f x
theorem Finset.subset_set_biUnion_of_mem {α : Type u_2} {β : Type u_3} {s : } {f : αSet β} {x : α} (h : x s) :
f x ⋃ y ∈ s, f y
theorem Finset.set_biUnion_union {α : Type u_2} {β : Type u_3} [] (s : ) (t : ) (u : αSet β) :
⋃ x ∈ s t, u x = (⋃ x ∈ s, u x) ⋃ x ∈ t, u x
theorem Finset.set_biInter_inter {α : Type u_2} {β : Type u_3} [] (s : ) (t : ) (u : αSet β) :
⋂ x ∈ s t, u x = (⋂ x ∈ s, u x) ⋂ x ∈ t, u x
theorem Finset.set_biUnion_insert {α : Type u_2} {β : Type u_3} [] (a : α) (s : ) (t : αSet β) :
⋃ x ∈ insert a s, t x = t a ⋃ x ∈ s, t x
theorem Finset.set_biInter_insert {α : Type u_2} {β : Type u_3} [] (a : α) (s : ) (t : αSet β) :
⋂ x ∈ insert a s, t x = t a ⋂ x ∈ s, t x
theorem Finset.set_biUnion_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {f : γα} {g : αSet β} {s : } :
⋃ x ∈ , g x = ⋃ y ∈ s, g (f y)
theorem Finset.set_biInter_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] {f : γα} {g : αSet β} {s : } :
⋂ x ∈ , g x = ⋂ y ∈ s, g (f y)
theorem Finset.set_biUnion_insert_update {α : Type u_2} {β : Type u_3} [] {x : α} {t : } (f : αSet β) {s : Set β} (hx : xt) :
⋃ i ∈ insert x t, Function.update f x s i = s ⋃ i ∈ t, f i
theorem Finset.set_biInter_insert_update {α : Type u_2} {β : Type u_3} [] {x : α} {t : } (f : αSet β) {s : Set β} (hx : xt) :
⋂ i ∈ insert x t, Function.update f x s i = s ⋂ i ∈ t, f i
theorem Finset.set_biUnion_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] (s : ) (t : γ) (f : αSet β) :
⋃ y ∈ , f y = ⋃ x ∈ s, ⋃ y ∈ t x, f y
theorem Finset.set_biInter_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] (s : ) (t : γ) (f : αSet β) :
⋂ y ∈ , f y = ⋂ x ∈ s, ⋂ y ∈ t x, f y