Lattice operations on finsets

sup

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

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

Equations

• s.sup f = Finset.fold (fun (x x_1 : α) => x ⊔ x_1) ⊥ f s

theorem Finset.sup_def {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} : s.sup f = (Multiset.map f s.val).sup

@[simp]

theorem Finset.sup_empty {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : β → α} : ∅.sup f = ⊥

@[simp]

theorem Finset.sup_cons {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {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} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} [DecidableEq β] {b : β} : (insert b s).sup f = f b ⊔ s.sup f

@[simp]

theorem Finset.sup_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] [DecidableEq β] (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} [SemilatticeSup α] [OrderBot α] (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} [SemilatticeSup α] [OrderBot α] {f : β → α} {b : β} : {b}.sup f = f b

theorem Finset.sup_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {g : β → α} : s.sup (f ⊔ g) = s.sup f ⊔ s.sup g

theorem Finset.sup_congr {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} {g : β → α} (hs : s₁ = s₂) (hfg : ∀ 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} [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [FunLike F α β] [SupBotHomClass F α β] (f : F) (s : Finset ι) (g : ι → α) : f (s.sup g) = s.sup (⇑f ∘ g)

@[simp]

theorem Finset.sup_le_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} : s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a

theorem Finset.sup_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} : (∀ 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} [SemilatticeSup α] [OrderBot α] {s : Finset β} {a : α} : (s.sup fun (x : β) => a) ≤ a

theorem Finset.le_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) : f b ≤ s.sup f

theorem Finset.le_sup_of_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup f

theorem Finset.sup_union {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} [DecidableEq β] : (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f

@[simp]

theorem Finset.sup_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] {f : β → α} [DecidableEq β] (s : Finset γ) (t : γ → Finset β) : (s.biUnion t).sup f = s.sup fun (x : γ) => (t x).sup f

theorem Finset.sup_const {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (c : α) : (s.sup fun (x : β) => c) = c

@[simp]

theorem Finset.sup_bot {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) : (s.sup fun (x : β) => ⊥) = ⊥

theorem Finset.sup_ite {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {g : β → α} (p : β → Prop) [DecidablePred p] : (s.sup fun (i : β) => if p i then f i else g i) = (Finset.filter p s).sup f ⊔ (Finset.filter (fun (i : β) => ¬p i) s).sup g

theorem Finset.sup_mono_fun {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.sup f ≤ s.sup g

theorem Finset.sup_mono {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) : s₁.sup f ≤ s₂.sup f

theorem Finset.sup_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β → γ → α) : (s.sup fun (b : β) => t.sup (f b)) = t.sup fun (c : γ) => s.sup fun (b : β) => f b c

@[simp]

theorem Finset.sup_attach {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) : (s.attach.sup fun (x : { x : β // x ∈ s }) => f ↑x) = s.sup f

theorem Finset.sup_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = s.sup fun (i : β) => t.sup fun (i' : γ) => f (i, i')

See also Finset.product_biUnion.

theorem Finset.sup_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = t.sup fun (i' : γ) => s.sup fun (i : β) => f (i, i')

@[simp]

theorem Finset.sup_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] [OrderBot α] [OrderBot β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).sup (Prod.map f g) = (s.sup f, t.sup g)

@[simp]

theorem Finset.sup_erase_bot {α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (s : Finset α) : (s.erase ⊥).sup id = s.sup id

theorem Finset.sup_sdiff_right {α : Type u_7} {β : Type u_8} [GeneralizedBooleanAlgebra α] (s : Finset β) (f : β → α) (a : α) : (s.sup fun (b : β) => f b \ a) = s.sup f \ a

theorem Finset.comp_sup_eq_sup_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] [SemilatticeSup γ] [OrderBot γ] {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} [SemilatticeSup α] [OrderBot α] {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 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} [DecidableEq β] (s : Finset α) (f : α → Multiset β) : (s.sup f).toFinset = s.sup fun (x : α) => (f x).toFinset

theorem List.foldr_sup_eq_sup_toFinset {α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (l : List α) : List.foldr (fun (x x_1 : α) => x ⊔ x_1) ⊥ l = l.toFinset.sup id

theorem Finset.subset_range_sup_succ (s : Finset ℕ) : s ⊆ Finset.range (s.sup id).succ

theorem Finset.exists_nat_subset_range (s : Finset ℕ) : ∃ (n : ℕ), s ⊆ Finset.range n

theorem Finset.sup_induction {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {p : α → Prop} (hb : p ⊥) (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) (hs : ∀ b ∈ s, p (f b)) : p (s.sup f)

theorem Finset.sup_le_of_le_directed {α : Type u_7} [SemilatticeSup α] [OrderBot α] (s : Set α) (hs : s.Nonempty) (hdir : DirectedOn (fun (x x_1 : α) => x ≤ x_1) s) (t : Finset α) : (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

theorem Finset.sup_mem {α : Type u_2} [SemilatticeSup α] [OrderBot α] (s : Set α) (w₁ : ⊥ ∈ s) (w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s) {ι : Type u_7} (t : Finset ι) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) : t.sup p ∈ s

@[simp]

theorem Finset.sup_eq_bot_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (f : β → α) (S : Finset β) : S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥

theorem Finset.sup_eq_iSup {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) : s.sup f = ⨆ a ∈ s, f a

theorem Finset.sup_id_eq_sSup {α : Type u_2} [CompleteLattice α] (s : Finset α) : s.sup id = sSup ↑s

theorem Finset.sup_id_set_eq_sUnion {α : Type u_2} (s : Finset (Set α)) : s.sup id = ⋃₀ ↑s

@[simp]

theorem Finset.sup_set_eq_biUnion {α : Type u_2} {β : Type u_3} (s : Finset α) (f : α → Set β) : s.sup f = ⋃ x ∈ s, f x

theorem Finset.sup_eq_sSup_image {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) : s.sup f = sSup (f '' ↑s)

inf

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

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

Equations

• s.inf f = Finset.fold (fun (x x_1 : α) => x ⊓ x_1) ⊤ f s

theorem Finset.inf_def {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} : s.inf f = (Multiset.map f s.val).inf

@[simp]

theorem Finset.inf_empty {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {f : β → α} : ∅.inf f = ⊤

@[simp]

theorem Finset.inf_cons {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {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} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} [DecidableEq β] {b : β} : (insert b s).inf f = f b ⊓ s.inf f

@[simp]

theorem Finset.inf_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] [DecidableEq β] (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} [SemilatticeInf α] [OrderTop α] (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} [SemilatticeInf α] [OrderTop α] {f : β → α} {b : β} : {b}.inf f = f b

theorem Finset.inf_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {g : β → α} : s.inf (f ⊓ g) = s.inf f ⊓ s.inf g

theorem Finset.inf_congr {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} {g : β → α} (hs : s₁ = s₂) (hfg : ∀ 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} [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [FunLike F α β] [InfTopHomClass F α β] (f : F) (s : Finset ι) (g : ι → α) : f (s.inf g) = s.inf (⇑f ∘ g)

@[simp]

theorem Finset.le_inf_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {a : α} : a ≤ s.inf f ↔ ∀ b ∈ s, a ≤ f b

theorem Finset.le_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {a : α} : (∀ 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} [SemilatticeInf α] [OrderTop α] {s : Finset β} {a : α} : a ≤ s.inf fun (x : β) => a

theorem Finset.inf_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) : s.inf f ≤ f b

theorem Finset.inf_le_of_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {a : α} {b : β} (hb : b ∈ s) (h : f b ≤ a) : s.inf f ≤ a

theorem Finset.inf_union {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} [DecidableEq β] : (s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f

@[simp]

theorem Finset.inf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] {f : β → α} [DecidableEq β] (s : Finset γ) (t : γ → Finset β) : (s.biUnion t).inf f = s.inf fun (x : γ) => (t x).inf f

theorem Finset.inf_const {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (h : s.Nonempty) (c : α) : (s.inf fun (x : β) => c) = c

@[simp]

theorem Finset.inf_top {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) : (s.inf fun (x : β) => ⊤) = ⊤

theorem Finset.inf_ite {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {g : β → α} (p : β → Prop) [DecidablePred p] : (s.inf fun (i : β) => if p i then f i else g i) = (Finset.filter p s).inf f ⊓ (Finset.filter (fun (i : β) => ¬p i) s).inf g

theorem Finset.inf_mono_fun {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.inf f ≤ s.inf g

theorem Finset.inf_mono {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) : s₂.inf f ≤ s₁.inf f

theorem Finset.inf_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β → γ → α) : (s.inf fun (b : β) => t.inf (f b)) = t.inf fun (c : γ) => s.inf fun (b : β) => f b c

theorem Finset.inf_attach {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α) : (s.attach.inf fun (x : { x : β // x ∈ s }) => f ↑x) = s.inf f

theorem Finset.inf_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).inf f = s.inf fun (i : β) => t.inf fun (i' : γ) => f (i, i')

theorem Finset.inf_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).inf f = t.inf fun (i' : γ) => s.inf fun (i : β) => f (i, i')

@[simp]

theorem Finset.inf_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] [OrderTop α] [OrderTop β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).inf (Prod.map f g) = (s.inf f, t.inf g)

@[simp]

theorem Finset.inf_erase_top {α : Type u_2} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (s : Finset α) : (s.erase ⊤).inf id = s.inf id

theorem Finset.comp_inf_eq_inf_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] [SemilatticeInf γ] [OrderTop γ] {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} [SemilatticeInf α] [OrderTop α] {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 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} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (l : List α) : List.foldr (fun (x x_1 : α) => x ⊓ x_1) ⊤ l = l.toFinset.inf id

theorem Finset.inf_induction {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {p : α → Prop} (ht : p ⊤) (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)) (hs : ∀ b ∈ s, p (f b)) : p (s.inf f)

theorem Finset.inf_mem {α : Type u_2} [SemilatticeInf α] [OrderTop α] (s : Set α) (w₁ : ⊤ ∈ s) (w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s) {ι : Type u_7} (t : Finset ι) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) : t.inf p ∈ s

@[simp]

theorem Finset.inf_eq_top_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (f : β → α) (S : Finset β) : S.inf f = ⊤ ↔ ∀ s ∈ S, f s = ⊤

@[simp]

theorem Finset.toDual_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) : OrderDual.toDual (s.sup f) = s.inf (⇑OrderDual.toDual ∘ f)

@[simp]

theorem Finset.toDual_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α) : OrderDual.toDual (s.inf f) = s.sup (⇑OrderDual.toDual ∘ f)

@[simp]

theorem Finset.ofDual_sup {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → αᵒᵈ) : OrderDual.ofDual (s.sup f) = s.inf (⇑OrderDual.ofDual ∘ f)

@[simp]

theorem Finset.ofDual_inf {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → αᵒᵈ) : OrderDual.ofDual (s.inf f) = s.sup (⇑OrderDual.ofDual ∘ f)

theorem Finset.sup_inf_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ι → α) (a : α) : a ⊓ s.sup f = s.sup fun (i : ι) => a ⊓ f i

theorem Finset.sup_inf_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ι → α) (a : α) : s.sup f ⊓ a = s.sup fun (i : ι) => f i ⊓ a

theorem Finset.disjoint_sup_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} : Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)

theorem Finset.disjoint_sup_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {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} [DistribLattice α] [OrderBot α] (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun (i : ι × κ) => f i.1 ⊓ g i.2

theorem Finset.inf_sup_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] (s : Finset ι) (f : ι → α) (a : α) : a ⊔ s.inf f = s.inf fun (i : ι) => a ⊔ f i

theorem Finset.inf_sup_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] (s : Finset ι) (f : ι → α) (a : α) : s.inf f ⊔ a = s.inf fun (i : ι) => f i ⊔ a

theorem Finset.codisjoint_inf_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] {f : ι → α} {s : Finset ι} {a : α} : Codisjoint a (s.inf f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Codisjoint a (f i)

theorem Finset.codisjoint_inf_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] {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} [DistribLattice α] [OrderTop α] (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : s.inf f ⊔ t.inf g = (s ×ˢ t).inf fun (i : ι × κ) => f i.1 ⊔ g i.2

theorem Finset.inf_sup {α : Type u_2} {ι : Type u_5} [DistribLattice α] [BoundedOrder α] [DecidableEq ι] {κ : ι → Type u_7} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : (s.inf fun (i : ι) => (t i).sup (f i)) = (s.pi t).sup fun (g : (a : ι) → a ∈ s → κ a) => s.attach.inf fun (i : { x : ι // x ∈ s }) => f (↑i) (g ↑i ⋯)

theorem Finset.sup_inf {α : Type u_2} {ι : Type u_5} [DistribLattice α] [BoundedOrder α] [DecidableEq ι] {κ : ι → Type u_7} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : (s.sup fun (i : ι) => (t i).inf (f i)) = (s.pi t).inf fun (g : (a : ι) → a ∈ s → κ a) => s.attach.sup fun (i : { x : ι // x ∈ s }) => f (↑i) (g ↑i ⋯)

theorem Finset.sup_sdiff_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α) : (s.sup fun (b : ι) => a \ f b) = a \ s.inf f

theorem Finset.inf_sdiff_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : (s.inf fun (b : ι) => a \ f b) = a \ s.sup f

theorem Finset.inf_sdiff_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : (s.inf fun (b : ι) => f b \ a) = s.inf f \ a

theorem Finset.inf_himp_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α) : (s.inf fun (b : ι) => f b ⇨ a) = s.sup f ⇨ a

theorem Finset.sup_himp_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : (s.sup fun (b : ι) => f b ⇨ a) = s.inf f ⇨ a

theorem Finset.sup_himp_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : (s.sup fun (b : ι) => a ⇨ f b) = a ⇨ s.sup f

@[simp]

theorem Finset.compl_sup {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) : (s.sup f)ᶜ = s.inf fun (i : ι) => (f i)ᶜ

@[simp]

theorem Finset.compl_inf {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) : (s.inf f)ᶜ = s.sup fun (i : ι) => (f i)ᶜ

theorem Finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} [SemilatticeSup β] [OrderBot β] (g : α → β) (mono_g : Monotone g) (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f)

@[simp]

theorem Finset.le_sup_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} (ha : ⊥ < a) : a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b

theorem Finset.sup_eq_top_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι} {f : ι → α} : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

theorem Finset.Nonempty.sup_eq_top_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

@[simp]

theorem Finset.lt_sup_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} : a < s.sup f ↔ ∃ b ∈ s, a < f b

@[simp]

theorem Finset.sup_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} (ha : ⊥ < a) : s.sup f < a ↔ ∀ b ∈ s, f b < a

theorem Finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} [SemilatticeInf β] [OrderTop β] (g : α → β) (mono_g : Monotone g) (top : g ⊤ = ⊤) : g (s.inf f) = s.inf (g ∘ f)

@[simp]

theorem Finset.inf_le_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} {a : α} (ha : a < ⊤) : s.inf f ≤ a ↔ ∃ b ∈ s, f b ≤ a

theorem Finset.inf_eq_bot_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι} {f : ι → α} : s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥

theorem Finset.Nonempty.inf_eq_bot_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ι → α} (h : s.Nonempty) : s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥

@[simp]

theorem Finset.inf_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} {a : α} : s.inf f < a ↔ ∃ b ∈ s, f b < a

@[simp]

theorem Finset.lt_inf_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} {a : α} (ha : a < ⊤) : a < s.inf f ↔ ∀ b ∈ s, a < f b

theorem Finset.inf_eq_iInf {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) : s.inf f = ⨅ a ∈ s, f a

theorem Finset.inf_id_eq_sInf {α : Type u_2} [CompleteLattice α] (s : Finset α) : s.inf id = sInf ↑s

theorem Finset.inf_id_set_eq_sInter {α : Type u_2} (s : Finset (Set α)) : s.inf id = ⋂₀ ↑s

@[simp]

theorem Finset.inf_set_eq_iInter {α : Type u_2} {β : Type u_3} (s : Finset α) (f : α → Set β) : s.inf f = ⋂ x ∈ s, f x

theorem Finset.inf_eq_sInf_image {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) : s.inf f = sInf (f '' ↑s)

theorem Finset.sup_of_mem {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) : ∃ (a : α), s.sup (WithBot.some ∘ f) = ↑a

def Finset.sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (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

• s.sup' H f = (s.sup (WithBot.some ∘ f)).unbot ⋯

@[simp]

theorem Finset.coe_sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) : ↑(s.sup' H f) = s.sup (WithBot.some ∘ f)

@[simp]

theorem Finset.sup'_cons {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β} {hb : b ∉ s} : (Finset.cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f

@[simp]

theorem Finset.sup'_insert {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) [DecidableEq β] {b : β} : (insert b s).sup' ⋯ f = f b ⊔ s.sup' H f

@[simp]

theorem Finset.sup'_singleton {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (f : β → α) {b : β} : {b}.sup' ⋯ f = f b

@[simp]

theorem Finset.sup'_le_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} : s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a

theorem Finset.sup'_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} : (∀ b ∈ s, f b ≤ a) → s.sup' H f ≤ a

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

theorem Finset.le_sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) : f b ≤ s.sup' ⋯ f

theorem Finset.le_sup'_of_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {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} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (a : α) : (s.sup' H fun (x : β) => a) = a

theorem Finset.sup'_union {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [DecidableEq β] {s₁ : Finset β} {s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : β → α) : (s₁ ∪ s₂).sup' ⋯ f = s₁.sup' h₁ f ⊔ s₂.sup' h₂ f

theorem Finset.sup'_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] (f : β → α) [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ (b : γ), (t b).Nonempty) : (s.biUnion t).sup' ⋯ f = s.sup' Hs fun (b : γ) => (t b).sup' ⋯ f

theorem Finset.sup'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β → γ → α) : (s.sup' hs fun (b : β) => t.sup' ht (f b)) = t.sup' ht fun (c : γ) => s.sup' hs fun (b : β) => f b c

theorem Finset.sup'_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).sup' h f = s.sup' ⋯ fun (i : β) => t.sup' ⋯ fun (i' : γ) => f (i, i')

theorem Finset.sup'_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).sup' h f = t.sup' ⋯ fun (i' : γ) => s.sup' ⋯ fun (i : β) => f (i, i')

theorem Finset.prodMk_sup'_sup' {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s.sup' hs f, t.sup' ht g) = (s ×ˢ t).sup' ⋯ (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} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' ⋯ f, t.sup' ⋯ g)

See also Finset.prodMk_sup'_sup'.

theorem Finset.sup'_induction {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {p : α → Prop} (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) (hs : ∀ b ∈ s, p (f b)) : p (s.sup' H f)

theorem Finset.sup'_mem {α : Type u_2} [SemilatticeSup α] (s : Set α) (w : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s) {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) : t.sup' H p ∈ s

theorem Finset.sup'_congr {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f : β → α} {g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) : s.sup' H f = t.sup' ⋯ g

theorem Finset.comp_sup'_eq_sup'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [SemilatticeSup γ] {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)

@[simp]

theorem map_finset_sup' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ι → α) : f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)

theorem Finset.nsmul_sup' {α : Type u_2} {β : Type u_3} [LinearOrderedAddCommMonoid β] {s : Finset α} (hs : s.Nonempty) (f : α → β) (n : ℕ) : (s.sup' hs fun (a : α) => n • f a) = n • s.sup' hs f

@[simp]

theorem Finset.sup'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (Finset.image f s).Nonempty) (g : β → α) : (Finset.image f s).sup' hs g = s.sup' ⋯ (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} [SemilatticeSup α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : s.Nonempty) (g : β → α) : s.sup' hs (g ∘ f) = (Finset.image f s).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} [SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (Finset.map f s).Nonempty) : (Finset.map f s).sup' hs g = s.sup' ⋯ (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} [SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) : s.sup' hs (g ∘ ⇑f) = (Finset.map f s).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} [SemilatticeSup α] (f : β → α) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) : s₁.sup' h₁ f ≤ s₂.sup' ⋯ f

theorem GCongr.finset_sup'_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (f : β → α) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ ⊆ s₂) {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} : s₁.sup' h₁ f ≤ s₂.sup' 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} [SemilatticeInf α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) : ∃ (a : α), s.inf (WithTop.some ∘ f) = ↑a

def Finset.inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (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

• s.inf' H f = (s.inf (WithTop.some ∘ f)).untop ⋯

@[simp]

theorem Finset.coe_inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) : ↑(s.inf' H f) = s.inf (WithTop.some ∘ f)

@[simp]

theorem Finset.inf'_cons {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β} {hb : b ∉ s} : (Finset.cons b s hb).inf' ⋯ f = f b ⊓ s.inf' H f

@[simp]

theorem Finset.inf'_insert {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) [DecidableEq β] {b : β} : (insert b s).inf' ⋯ f = f b ⊓ s.inf' H f

@[simp]

theorem Finset.inf'_singleton {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (f : β → α) {b : β} : {b}.inf' ⋯ f = f b

@[simp]

theorem Finset.le_inf'_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} : a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b

theorem Finset.le_inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} (hs : ∀ b ∈ s, a ≤ f b) : a ≤ s.inf' H f

theorem Finset.inf'_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) : s.inf' ⋯ f ≤ f b

theorem Finset.inf'_le_of_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {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} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (a : α) : (s.inf' H fun (x : β) => a) = a

theorem Finset.inf'_union {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [DecidableEq β] {s₁ : Finset β} {s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : β → α) : (s₁ ∪ s₂).inf' ⋯ f = s₁.inf' h₁ f ⊓ s₂.inf' h₂ f

theorem Finset.inf'_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] (f : β → α) [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ (b : γ), (t b).Nonempty) : (s.biUnion t).inf' ⋯ f = s.inf' Hs fun (b : γ) => (t b).inf' ⋯ f

theorem Finset.inf'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β → γ → α) : (s.inf' hs fun (b : β) => t.inf' ht (f b)) = t.inf' ht fun (c : γ) => s.inf' hs fun (b : β) => f b c

theorem Finset.inf'_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).inf' h f = s.inf' ⋯ fun (i : β) => t.inf' ⋯ fun (i' : γ) => f (i, i')

theorem Finset.inf'_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).inf' h f = t.inf' ⋯ fun (i' : γ) => s.inf' ⋯ fun (i : β) => f (i, i')

theorem Finset.prodMk_inf'_inf' {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s.inf' hs f, t.inf' ht g) = (s ×ˢ t).inf' ⋯ (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} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).inf' hst (Prod.map f g) = (s.inf' ⋯ f, t.inf' ⋯ g)

See also Finset.prodMk_inf'_inf'.

theorem Finset.comp_inf'_eq_inf'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [SemilatticeInf γ] {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} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {p : α → Prop} (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)) (hs : ∀ b ∈ s, p (f b)) : p (s.inf' H f)

theorem Finset.inf'_mem {α : Type u_2} [SemilatticeInf α] (s : Set α) (w : ∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s) {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) : t.inf' H p ∈ s

theorem Finset.inf'_congr {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f : β → α} {g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) : s.inf' H f = t.inf' ⋯ g

@[simp]

theorem map_finset_inf' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ι → α) : f (s.inf' hs g) = s.inf' hs (⇑f ∘ g)

theorem Finset.nsmul_inf' {α : Type u_2} {β : Type u_3} [LinearOrderedAddCommMonoid β] {s : Finset α} (hs : s.Nonempty) (f : α → β) (n : ℕ) : (s.inf' hs fun (a : α) => n • f a) = n • s.inf' hs f

@[simp]

theorem Finset.inf'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (Finset.image f s).Nonempty) (g : β → α) : (Finset.image f s).inf' hs g = s.inf' ⋯ (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} [SemilatticeInf α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : s.Nonempty) (g : β → α) : s.inf' hs (g ∘ f) = (Finset.image f s).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} [SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (Finset.map f s).Nonempty) : (Finset.map f s).inf' hs g = s.inf' ⋯ (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} [SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) : s.inf' hs (g ∘ ⇑f) = (Finset.map f s).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} [SemilatticeInf α] (f : β → α) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) : s₂.inf' ⋯ f ≤ s₁.inf' h₁ f

theorem GCongr.finset_inf'_mono {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (f : β → α) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ ⊆ s₂) {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} : s₂.inf' h₂ f ≤ s₁.inf' 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} [SemilatticeSup α] [OrderBot α] {s : Finset β} (H : s.Nonempty) (f : β → α) : s.sup' H f = s.sup f

theorem Finset.coe_sup_of_nonempty {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (f : β → α) : ↑(s.sup f) = s.sup (WithBot.some ∘ f)

theorem Finset.inf'_eq_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (H : s.Nonempty) (f : β → α) : s.inf' H f = s.inf f

theorem Finset.coe_inf_of_nonempty {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (h : s.Nonempty) (f : β → α) : ↑(s.inf f) = s.inf (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 : Finset α) (f : α → (b : β) → C b) (b : β) : s.sup f b = s.sup 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 : Finset α) (f : α → (b : β) → C b) (b : β) : s.inf f b = s.inf 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 : Finset α} (H : s.Nonempty) (f : α → (b : β) → C b) (b : β) : s.sup' H f b = s.sup' 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 : Finset α} (H : s.Nonempty) (f : α → (b : β) → C b) (b : β) : s.inf' H f b = s.inf' H fun (a : α) => f a b

@[simp]

theorem Finset.toDual_sup' {α : Type u_2} {ι : Type u_5} [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) : OrderDual.toDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.toDual ∘ f)

@[simp]

theorem Finset.toDual_inf' {α : Type u_2} {ι : Type u_5} [SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) : OrderDual.toDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.toDual ∘ f)

@[simp]

theorem Finset.ofDual_sup' {α : Type u_2} {ι : Type u_5} [SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ι → αᵒᵈ) : OrderDual.ofDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.ofDual ∘ f)

@[simp]

theorem Finset.ofDual_inf' {α : Type u_2} {ι : Type u_5} [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ι → αᵒᵈ) : OrderDual.ofDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.ofDual ∘ f)

theorem Finset.sup'_inf_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : a ⊓ s.sup' hs f = s.sup' hs fun (i : ι) => a ⊓ f i

theorem Finset.sup'_inf_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : s.sup' hs f ⊓ a = s.sup' hs fun (i : ι) => f i ⊓ a

theorem Finset.sup'_inf_sup' {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → α) : s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun (i : ι × κ) => f i.1 ⊓ g i.2

theorem Finset.inf'_sup_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : a ⊔ s.inf' hs f = s.inf' hs fun (i : ι) => a ⊔ f i

theorem Finset.inf'_sup_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : s.inf' hs f ⊔ a = s.inf' hs fun (i : ι) => f i ⊔ a

theorem Finset.inf'_sup_inf' {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → α) : s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' ⋯ fun (i : ι × κ) => f i.1 ⊔ g i.2

@[simp]

theorem Finset.le_sup'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} : a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b

@[simp]

theorem Finset.lt_sup'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} : a < s.sup' H f ↔ ∃ b ∈ s, a < f b

@[simp]

theorem Finset.sup'_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} : s.sup' H f < a ↔ ∀ i ∈ s, f i < a

@[simp]

theorem Finset.inf'_le_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} : s.inf' H f ≤ a ↔ ∃ i ∈ s, f i ≤ a

@[simp]

theorem Finset.inf'_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} : s.inf' H f < a ↔ ∃ i ∈ s, f i < a

@[simp]

theorem Finset.lt_inf'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} : a < s.inf' H f ↔ ∀ i ∈ s, a < f i

theorem Finset.exists_mem_eq_sup' {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ι → α) : ∃ i ∈ s, s.sup' H f = f i

theorem Finset.exists_mem_eq_inf' {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ι → α) : ∃ i ∈ s, s.inf' H f = f i

theorem Finset.exists_mem_eq_sup {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) : ∃ i ∈ s, s.sup f = f i

theorem Finset.exists_mem_eq_inf {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) : ∃ i ∈ s, s.inf f = f i

max and min of finite sets

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

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

• s.max = s.sup WithBot.some

theorem Finset.max_eq_sup_coe {α : Type u_2} [LinearOrder α] {s : Finset α} : s.max = s.sup WithBot.some

theorem Finset.max_eq_sup_withBot {α : Type u_2} [LinearOrder α] (s : Finset α) : s.max = s.sup WithBot.some

@[simp]

theorem Finset.max_empty {α : Type u_2} [LinearOrder α] : ∅.max = ⊥

@[simp]

theorem Finset.max_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} : (insert a s).max = max (↑a) s.max

@[simp]

theorem Finset.max_singleton {α : Type u_2} [LinearOrder α] {a : α} : {a}.max = ↑a

theorem Finset.max_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a ∈ s) : ∃ (b : α), s.max = ↑b

theorem Finset.max_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) : ∃ (a : α), s.max = ↑a

theorem Finset.max_eq_bot {α : Type u_2} [LinearOrder α] {s : Finset α} : s.max = ⊥ ↔ s = ∅

theorem Finset.mem_of_max {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} : s.max = ↑a → a ∈ s

theorem Finset.le_max {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a ∈ s) : ↑a ≤ s.max

theorem Finset.not_mem_of_max_lt_coe {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : s.max < ↑a) : a ∉ s

theorem Finset.le_max_of_eq {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : a ∈ s) (h₂ : s.max = ↑b) : a ≤ b

theorem Finset.not_mem_of_max_lt {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : b < a) (h₂ : s.max = ↑b) : a ∉ s

theorem Finset.max_mono {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (st : s ⊆ t) : s.max ≤ t.max

theorem Finset.max_le {α : Type u_2} [LinearOrder α] {M : WithBot α} {s : Finset α} (st : ∀ a ∈ s, ↑a ≤ M) : s.max ≤ M

@[simp]

theorem Finset.max_le_iff {α : Type u_2} [LinearOrder α] {m : WithBot α} {s : Finset α} : s.max ≤ m ↔ ∀ a ∈ s, ↑a ≤ m

@[simp]

theorem Finset.max_eq_top {α : Type u_2} [LinearOrder α] [OrderTop α] {s : Finset α} : s.max = ⊤ ↔ ⊤ ∈ s

def Finset.min {α : Type u_2} [LinearOrder α] (s : Finset α) : WithTop α

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

• s.min = s.inf WithTop.some

theorem Finset.min_eq_inf_withTop {α : Type u_2} [LinearOrder α] (s : Finset α) : s.min = s.inf WithTop.some

@[simp]

theorem Finset.min_empty {α : Type u_2} [LinearOrder α] : ∅.min = ⊤

@[simp]

theorem Finset.min_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} : (insert a s).min = min (↑a) s.min

@[simp]

theorem Finset.min_singleton {α : Type u_2} [LinearOrder α] {a : α} : {a}.min = ↑a

theorem Finset.min_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a ∈ s) : ∃ (b : α), s.min = ↑b

theorem Finset.min_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) : ∃ (a : α), s.min = ↑a

@[simp]

theorem Finset.min_eq_top {α : Type u_2} [LinearOrder α] {s : Finset α} : s.min = ⊤ ↔ s = ∅

theorem Finset.mem_of_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} : s.min = ↑a → a ∈ s

theorem Finset.min_le {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a ∈ s) : s.min ≤ ↑a

theorem Finset.not_mem_of_coe_lt_min {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : ↑a < s.min) : a ∉ s

theorem Finset.min_le_of_eq {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : b ∈ s) (h₂ : s.min = ↑a) : a ≤ b

theorem Finset.not_mem_of_lt_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : a < b) (h₂ : s.min = ↑b) : a ∉ s

theorem Finset.min_mono {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (st : s ⊆ t) : t.min ≤ s.min

theorem Finset.le_min {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} (st : ∀ a ∈ s, m ≤ ↑a) : m ≤ s.min

@[simp]

theorem Finset.le_min_iff {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} : m ≤ s.min ↔ ∀ a ∈ s, m ≤ ↑a

@[simp]

theorem Finset.min_eq_bot {α : Type u_2} [LinearOrder α] [OrderBot α] {s : Finset α} : s.min = ⊥ ↔ ⊥ ∈ s

def Finset.min' {α : Type u_2} [LinearOrder α] (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 WithTop α.

Equations

• s.min' H = s.inf' H id

def Finset.max' {α : Type u_2} [LinearOrder α] (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 WithBot α.

Equations

• s.max' H = s.sup' H id

theorem Finset.min'_mem {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.min' H ∈ s

theorem Finset.min'_le {α : Type u_2} [LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s) : s.min' ⋯ ≤ x

theorem Finset.le_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α) (H2 : ∀ y ∈ s, x ≤ y) : x ≤ s.min' H

theorem Finset.isLeast_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : IsLeast (↑s) (s.min' H)

@[simp]

theorem Finset.le_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y

@[simp]

theorem Finset.min'_singleton {α : Type u_2} [LinearOrder α] (a : α) : {a}.min' ⋯ = a

{a}.min' _ is a.

theorem Finset.max'_mem {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.max' H ∈ s

theorem Finset.le_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s) : x ≤ s.max' ⋯

theorem Finset.max'_le {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α) (H2 : ∀ y ∈ s, y ≤ x) : s.max' H ≤ x

theorem Finset.isGreatest_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : IsGreatest (↑s) (s.max' H)

@[simp]

theorem Finset.max'_le_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x

@[simp]

theorem Finset.max'_lt_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : s.max' H < x ↔ ∀ y ∈ s, y < x

@[simp]

theorem Finset.lt_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : x < s.min' H ↔ ∀ y ∈ s, x < y

theorem Finset.max'_eq_sup' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.max' H = s.sup' H id

theorem Finset.min'_eq_inf' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.min' H = s.inf' H id

@[simp]

theorem Finset.max'_singleton {α : Type u_2} [LinearOrder α] (a : α) : {a}.max' ⋯ = a

{a}.max' _ is a.

theorem Finset.min'_lt_max' {α : Type u_2} [LinearOrder α] (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} [LinearOrder α] (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.map_ofDual_min {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) : WithTop.map (⇑OrderDual.ofDual) s.min = (Finset.image (⇑OrderDual.ofDual) s).max

theorem Finset.map_ofDual_max {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) : WithBot.map (⇑OrderDual.ofDual) s.max = (Finset.image (⇑OrderDual.ofDual) s).min

theorem Finset.map_toDual_min {α : Type u_2} [LinearOrder α] (s : Finset α) : WithTop.map (⇑OrderDual.toDual) s.min = (Finset.image (⇑OrderDual.toDual) s).max

theorem Finset.map_toDual_max {α : Type u_2} [LinearOrder α] (s : Finset α) : WithBot.map (⇑OrderDual.toDual) s.max = (Finset.image (⇑OrderDual.toDual) s).min

theorem Finset.ofDual_min' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) : OrderDual.ofDual (s.min' hs) = (Finset.image (⇑OrderDual.ofDual) s).max' ⋯

theorem Finset.ofDual_max' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) : OrderDual.ofDual (s.max' hs) = (Finset.image (⇑OrderDual.ofDual) s).min' ⋯

theorem Finset.toDual_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : OrderDual.toDual (s.min' hs) = (Finset.image (⇑OrderDual.toDual) s).max' ⋯

theorem Finset.toDual_max' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : OrderDual.toDual (s.max' hs) = (Finset.image (⇑OrderDual.toDual) s).min' ⋯

theorem Finset.max'_subset {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) : s.max' H ≤ t.max' ⋯

theorem Finset.min'_subset {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) : t.min' ⋯ ≤ s.min' H

theorem Finset.max'_insert {α : Type u_2} [LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty) : (insert a s).max' ⋯ = max (s.max' H) a

theorem Finset.min'_insert {α : Type u_2} [LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty) : (insert a s).min' ⋯ = min (s.min' H) a

theorem Finset.lt_max'_of_mem_erase_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) [DecidableEq α] {a : α} (ha : a ∈ s.erase (s.max' H)) : a < s.max' H

theorem Finset.min'_lt_of_mem_erase_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) [DecidableEq α] {a : α} (ha : a ∈ s.erase (s.min' H)) : s.min' H < a

@[simp]

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

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

theorem Monotone.map_finset_max' {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) : f (s.max' h) = (Finset.image f s).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} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α) (h : (Finset.image f s).Nonempty) : (Finset.image f s).min' h = f (s.min' ⋯)

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

theorem Monotone.map_finset_min' {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) : f (s.min' h) = (Finset.image f s).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} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : ↑(s.max' hs) = s.max

theorem Finset.coe_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : ↑(s.min' hs) = s.min

theorem Finset.max_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : s.max ∈ Finset.image WithBot.some s

theorem Finset.min_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : s.min ∈ Finset.image WithTop.some s

theorem Finset.max_mem_insert_bot_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) : s.max ∈ insert ⊥ (Finset.image WithBot.some s)

theorem Finset.min_mem_insert_top_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) : s.min ∈ insert ⊤ (Finset.image WithTop.some s)

theorem Finset.max'_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).max' s0 ≠ x

theorem Finset.min'_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).min' s0 ≠ x

theorem Finset.max_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} : (s.erase x).max ≠ ↑x

theorem Finset.min_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} : (s.erase x).min ≠ ↑x

theorem Finset.exists_next_right {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) : ∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z

theorem Finset.exists_next_left {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (h : ∃ y ∈ s, y < x) : ∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y

theorem Finset.card_le_of_interleaved {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.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} [LinearOrder α] {s : Finset α} {t : Finset α} (h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.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} [LinearOrder α] [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅) (step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (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} [LinearOrder α] [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅) (step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, a < x) → p s → p (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} [LinearOrder α] [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅) (step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (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} [LinearOrder α] [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅) (step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f a ≤ f x) → p s → p (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} [LinearOrder α] (s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

theorem Finset.exists_min_image {α : Type u_2} {β : Type u_3} [LinearOrder α] (s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x'

theorem Finset.isGLB_iff_isLeast {α : Type u_2} [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) : IsGLB (↑s) i ↔ IsLeast (↑s) i

theorem Finset.isLUB_iff_isGreatest {α : Type u_2} [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) : IsLUB (↑s) i ↔ IsGreatest (↑s) i

theorem Finset.isGLB_mem {α : Type u_2} [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (↑s) i) (hs : s.Nonempty) : i ∈ s

theorem Finset.isLUB_mem {α : Type u_2} [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (↑s) i) (hs : s.Nonempty) : i ∈ s

theorem Multiset.map_finset_sup {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] [DecidableEq β] (s : Finset γ) (f : γ → Multiset β) (g : β → α) (hg : Function.Injective g) : Multiset.map g (s.sup f) = s.sup (Multiset.map g ∘ f)

theorem Multiset.count_finset_sup {α : Type u_2} {β : Type u_3} [DecidableEq β] (s : Finset α) (f : α → Multiset β) (b : β) : Multiset.count b (s.sup f) = s.sup fun (a : α) => Multiset.count b (f a)

theorem Multiset.mem_sup {α : Type u_7} {β : Type u_8} [DecidableEq β] {s : Finset α} {f : α → Multiset β} {x : β} : x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v

theorem Finset.mem_sup {α : Type u_7} {β : Type u_8} [DecidableEq β] {s : Finset α} {f : α → Finset β} {x : β} : x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v

theorem Finset.sup_eq_biUnion {α : Type u_7} {β : Type u_8} [DecidableEq β] (s : Finset α) (t : α → Finset β) : s.sup t = s.biUnion t

@[simp]

theorem Finset.sup_singleton'' {α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset β) (f : β → α) : (s.sup fun (b : β) => {f b}) = Finset.image f s

@[simp]

theorem Finset.sup_singleton' {α : Type u_2} [DecidableEq α] (s : Finset α) : s.sup singleton = s

theorem iSup_eq_iSup_finset {α : Type u_2} {ι : Type u_5} [CompleteLattice α] (s : ι → α) : ⨆ (i : ι), s i = ⨆ (t : Finset ι), ⨆ 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} [CompleteLattice α] (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} [CompleteLattice α] (s : ι → α) : ⨅ (i : ι), s i = ⨅ (t : Finset ι), ⨅ 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} [CompleteLattice α] (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 : Finset ι), ⋃ 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 : Finset ι), ⋂ 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.

theorem Finset.mem_maximals_iff_forall_insert {α : Type u_2} [DecidableEq α] {P : Finset α → Prop} {s : Finset α} (hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s) : s ∈ maximals (fun (x x_1 : Finset α) => x ⊆ x_1) {t : Finset α | P t} ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

theorem Finset.mem_minimals_iff_forall_erase {α : Type u_2} [DecidableEq α] {P : Finset α → Prop} {s : Finset α} (hP : ∀ ⦃s t : Finset α⦄, P s → s ⊆ t → P t) : s ∈ minimals (fun (x x_1 : Finset α) => x ⊆ x_1) {t : Finset α | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s.erase x)

Interaction with big lattice/set operations

theorem Finset.iSup_coe {α : Type u_2} {β : Type u_3} [SupSet β] (f : α → β) (s : Finset α) : ⨆ x ∈ ↑s, f x = ⨆ x ∈ s, f x

theorem Finset.iInf_coe {α : Type u_2} {β : Type u_3} [InfSet β] (f : α → β) (s : Finset α) : ⨅ x ∈ ↑s, f x = ⨅ x ∈ s, f x

theorem Finset.iSup_singleton {α : Type u_2} {β : Type u_3} [CompleteLattice β] (a : α) (s : α → β) : ⨆ x ∈ {a}, s x = s a

theorem Finset.iInf_singleton {α : Type u_2} {β : Type u_3} [CompleteLattice β] (a : α) (s : α → β) : ⨅ x ∈ {a}, s x = s a

theorem Finset.iSup_option_toFinset {α : Type u_2} {β : Type u_3} [CompleteLattice β] (o : Option α) (f : α → β) : ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

theorem Finset.iInf_option_toFinset {α : Type u_2} {β : Type u_3} [CompleteLattice β] (o : Option α) (f : α → β) : ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x

theorem Finset.iSup_union {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {f : α → β} {s : Finset α} {t : Finset α} : ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

theorem Finset.iInf_union {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {f : α → β} {s : Finset α} {t : Finset α} : ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x

theorem Finset.iSup_insert {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] (a : α) (s : Finset α) (t : α → β) : ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

theorem Finset.iInf_insert {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] (a : α) (s : Finset α) (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} [CompleteLattice β] [DecidableEq α] {f : γ → α} {g : α → β} {s : Finset γ} : ⨆ x ∈ Finset.image f s, g x = ⨆ y ∈ s, g (f y)

theorem Finset.iInf_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] {f : γ → α} {g : α → β} {s : Finset γ} : ⨅ x ∈ Finset.image f s, g x = ⨅ y ∈ s, g (f y)

theorem Finset.iSup_insert_update {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) : ⨆ 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} [CompleteLattice β] [DecidableEq α] {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) : ⨅ 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} [CompleteLattice β] [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → β) : ⨆ y ∈ s.biUnion t, f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y

theorem Finset.iInf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → β) : ⨅ y ∈ s.biUnion t, f y = ⨅ x ∈ s, ⨅ y ∈ t x, f y

theorem Finset.set_biUnion_coe {α : Type u_2} {β : Type u_3} (s : Finset α) (t : α → Set β) : ⋃ x ∈ ↑s, t x = ⋃ x ∈ s, t x

theorem Finset.set_biInter_coe {α : Type u_2} {β : Type u_3} (s : Finset α) (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 : Finset β) : ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' ↑s

theorem Finset.set_biUnion_option_toFinset {α : Type u_2} {β : Type u_3} (o : Option α) (f : α → Set β) : ⋃ x ∈ o.toFinset, f x = ⋃ x ∈ o, f x

theorem Finset.set_biInter_option_toFinset {α : Type u_2} {β : Type u_3} (o : Option α) (f : α → Set β) : ⋂ x ∈ o.toFinset, f x = ⋂ x ∈ o, f x

theorem Finset.subset_set_biUnion_of_mem {α : Type u_2} {β : Type u_3} {s : Finset α} {f : α → Set β} {x : α} (h : x ∈ s) : f x ⊆ ⋃ y ∈ s, f y

theorem Finset.set_biUnion_union {α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset α) (t : Finset α) (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} [DecidableEq α] (s : Finset α) (t : Finset α) (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} [DecidableEq α] (a : α) (s : Finset α) (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} [DecidableEq α] (a : α) (s : Finset α) (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} [DecidableEq α] {f : γ → α} {g : α → Set β} {s : Finset γ} : ⋃ x ∈ Finset.image f s, g x = ⋃ y ∈ s, g (f y)

theorem Finset.set_biInter_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] {f : γ → α} {g : α → Set β} {s : Finset γ} : ⋂ x ∈ Finset.image f s, g x = ⋂ y ∈ s, g (f y)

theorem Finset.set_biUnion_insert_update {α : Type u_2} {β : Type u_3} [DecidableEq α] {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) : ⋃ 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} [DecidableEq α] {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) : ⋂ 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} [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → Set β) : ⋃ y ∈ s.biUnion t, f y = ⋃ x ∈ s, ⋃ y ∈ t x, f y

theorem Finset.set_biInter_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → Set β) : ⋂ y ∈ s.biUnion t, f y = ⋂ x ∈ s, ⋂ y ∈ t x, f y