Loogle!
Result
Found 353 declarations mentioning Finset.sup. Of these, only the first 200 are shown.
- Finset.sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) : α - Finset.subset_range_sup_succ 📋 Mathlib.Data.Finset.Lattice.Fold
(s : Finset ℕ) : s ⊆ Finset.range (s.sup id).succ - Finset.sup_singleton_eq_self 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} [DecidableEq α] (s : Finset α) : s.sup singleton = s - Finset.sup_const 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (c : α) : (s.sup fun x => c) = c - Finset.sup_singleton 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : β → α} {b : β} : {b}.sup f = f b - Finset.sup_const_le 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {a : α} : (s.sup fun x => a) ≤ a - Finset.sup'_eq_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (H : s.Nonempty) (f : β → α) : s.sup' H f = s.sup f - Finset.sup_def 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} : s.sup f = (Multiset.map f s.val).sup - Finset.isLUB_sup_id 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} [SemilatticeSup α] [OrderBot α] {s : Finset α} : IsLUB (↑s) (s.sup id) - Finset.monotone_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (f : β → α) : Monotone fun s => s.sup f - Finset.sup_singleton_apply 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset β) (f : β → α) : (s.sup fun b => {f b}) = Finset.image f s - Finset.sup_empty 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : β → α} : ∅.sup f = ⊥ - Finset.sup_eq_bot_of_isEmpty 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] [IsEmpty β] (f : β → α) (S : Finset β) : S.sup f = ⊥ - Finset.isLUB_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} : IsLUB (f '' ↑s) (s.sup f) - Multiset.count_finset_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.coe_sup' 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) : ↑(s.sup' H f) = s.sup (WithBot.some ∘ f) - Finset.exists_sup_ge 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup β] [OrderBot β] [WellFoundedGT β] (f : α → β) : ∃ t, ∀ (a : α), f a ≤ t.sup f - Finset.le_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) : f b ≤ s.sup f - Finset.sup_bot 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) : (s.sup fun x => ⊥) = ⊥ - Finset.sup_id_eq_sSup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} [CompleteLattice α] (s : Finset α) : s.sup id = sSup ↑s - Finset.sup_image 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.sup_toFinset 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_6} {β : Type u_7} [DecidableEq β] (s : Finset α) (f : α → Multiset β) : (s.sup f).toFinset = s.sup fun x => (f x).toFinset - Finset.sup_erase_bot 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (s : Finset α) : (s.erase ⊥).sup id = s.sup id - BddAbove.range_finsetSup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : β → α} (hf : BddAbove (Set.range f)) : BddAbove (Set.range fun s => s.sup f) - Finset.sup_insert 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} [DecidableEq β] {b : β} : (insert b s).sup f = f b ⊔ s.sup f - Finset.sup_eq_sSup_image 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) : s.sup f = sSup (f '' ↑s) - List.foldr_sup_eq_sup_toFinset 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (l : List α) : List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l = l.toFinset.sup id - Finset.sup_comm 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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 - Finset.sup_mono 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) : s₁.sup f ≤ s₂.sup f - Finset.sup_of_mem 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) : ∃ a, s.sup (WithBot.some ∘ f) = ↑a - Finset.sup_sdiff_right 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_6} {β : Type u_7} [GeneralizedBooleanAlgebra α] (s : Finset β) (f : β → α) (a : α) : (s.sup fun b => f b \ a) = s.sup f \ a - Finset.sup_map 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.sup_mem_of_nonempty 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) : s.sup f ∈ f '' ↑s - Finset.sup_union 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f : β → α} [DecidableEq β] : (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f - Finset.coe_sup_of_nonempty 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (f : β → α) : ↑(s.sup f) = s.sup (WithBot.some ∘ f) - Multiset.mem_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_6} {β : Type u_7} [DecidableEq β] {s : Finset α} {f : α → Multiset β} {x : β} : x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v - Finset.sup_cons 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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 - Finset.exists_mem_eq_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) : ∃ i ∈ s, s.sup f = f i - Finset.sup_id_set_eq_sUnion 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} (s : Finset (Set α)) : s.sup id = ⋃₀ ↑s - Finset.sup_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f g : β → α} : s.sup (f ⊔ g) = s.sup f ⊔ s.sup g - Finset.le_sup_of_le 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup f - Finset.sup_le 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} : (∀ b ∈ s, f b ≤ a) → s.sup f ≤ a - Finset.exists_sup_eq_iSup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [CompleteLattice β] [WellFoundedGT β] (f : α → β) : ∃ t, t.sup f = ⨆ a, f a - Finset.sup_congr 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) : s₁.sup f = s₂.sup g - Finset.sup_le_iff 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} : s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a - Multiset.map_finset_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.mem_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} : a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i - Finset.sup_disjSum 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β ⊕ γ → α) : (s.disjSum t).sup f = (s.sup fun x => f (Sum.inl x)) ⊔ t.sup fun x => f (Sum.inr x) - Finset.compl_inf 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) : (s.inf f)ᶜ = s.sup fun i => (f i)ᶜ - Finset.compl_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) : (s.sup f)ᶜ = s.inf fun i => (f i)ᶜ - Finset.sup_eq_bot_iff 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (f : β → α) (S : Finset β) : S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥ - Finset.sup_eq_one 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} [One α] [IsBotOneClass α] : s.sup f = 1 ↔ ∀ i ∈ s, f i = 1 - Finset.sup_eq_zero 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} [Zero α] [IsBotZeroClass α] : s.sup f = 0 ↔ ∀ i ∈ s, f i = 0 - Finset.sup_inf_distrib_left 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ι → α) (a : α) : a ⊓ s.sup f = s.sup fun i => a ⊓ f i - Finset.sup_inf_distrib_right 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ι → α) (a : α) : s.sup f ⊓ a = s.sup fun i => f i ⊓ a - Finset.sup_mono_fun 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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 - Finset.sup_induction 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.disjoint_sup_left 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} : Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint (f i) a - Finset.disjoint_sup_right 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} : Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i) - Finset.inf_himp_right 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α) : (s.inf fun b => f b ⇨ a) = s.sup f ⇨ a - Finset.sup_sdiff_left 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α) : (s.sup fun b => a \ f b) = a \ s.inf f - Finset.inf_sdiff_left 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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 - Finset.sup_apply 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} {C : β → Type u_6} [(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 - Finset.sup_himp_left 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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 - Finset.sup_himp_right 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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 - Finset.sup_eq_iSup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) : s.sup f = ⨆ a ∈ s, f a - Finset.sup_ite 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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 ⊔ {i ∈ s | ¬p i}.sup g - Finset.sup_set_eq_biUnion 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} (s : Finset α) (f : α → Set β) : s.sup f = ⋃ x ∈ s, f x - Finset.le_sup_dite_pos 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β} (h₀ : b ∈ s) (h₁ : p b) : f b h₁ ≤ s.sup fun i => if h : p i then f i h else g i h - Finset.sup_attach 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) : (s.attach.sup fun x => f ↑x) = s.sup f - Finset.le_sup_dite_neg 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β} (h₀ : b ∈ s) (h₁ : ¬p b) : g b h₁ ≤ s.sup fun i => if h : p i then f i h else g i h - Finset.apply_sup_eq_sup_comp_of_nonempty 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] {s : Finset ι} {f : ι → α} [OrderBot α] [SemilatticeSup β] [OrderBot β] {g : α → β} (mono_g : Monotone g) (H : s.Nonempty) : g (s.sup f) = s.sup (g ∘ f) - Finset.comp_sup_eq_sup_comp_of_nonempty 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] {s : Finset ι} {f : ι → α} [OrderBot α] [SemilatticeSup β] [OrderBot β] {g : α → β} (mono_g : Monotone g) (H : s.Nonempty) : g (s.sup f) = s.sup (g ∘ f) - Finset.lt_sup_iff 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} : a < s.sup f ↔ ∃ b ∈ s, a < f b - Finset.sup_coe 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.toDual_inf 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α) : OrderDual.toDual (s.inf f) = s.sup (⇑OrderDual.toDual ∘ f) - Finset.toDual_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) : OrderDual.toDual (s.sup f) = s.inf (⇑OrderDual.toDual ∘ f) - Finset.ofDual_inf 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → αᵒᵈ) : OrderDual.ofDual (s.inf f) = s.sup (⇑OrderDual.ofDual ∘ f) - Finset.ofDual_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → αᵒᵈ) : OrderDual.ofDual (s.sup f) = s.inf (⇑OrderDual.ofDual ∘ f) - map_finset_sup 📋 Mathlib.Data.Finset.Lattice.Fold
{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) - Finset.apply_sup_eq_sup_comp 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.comp_sup_eq_sup_comp 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.sup_le_of_le_directed 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_6} [SemilatticeSup α] [OrderBot α] (s : Set α) (hs : s.Nonempty) (hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s) (t : Finset α) : (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x - Finset.sup_mem 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} [SemilatticeSup α] [OrderBot α] (s : Set α) (w₁ : ⊥ ∈ s) (w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s) {ι : Type u_6} (t : Finset ι) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) : t.sup p ∈ s - Finset.apply_sup_eq_sup_comp_of_linearOrder 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.comp_sup_eq_sup_comp_of_is_total 📋 Mathlib.Data.Finset.Lattice.Fold
{α : 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) - Finset.sup_lt_iff 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} (ha : ⊥ < a) : s.sup f < a ↔ ∀ b ∈ s, f b < a - Finset.le_sup_iff 📋 Mathlib.Data.Finset.Lattice.Fold
{α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} (ha : ⊥ < a) : a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b - Finset.sup_eq_top_iff 📋 Mathlib.Data.Finset.Lattice.Fold
{ι : Type u_5} {α : Type u_6} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι} {f : ι → α} : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤ - Finset.Nonempty.sup_eq_top_iff 📋 Mathlib.Data.Finset.Lattice.Fold
{ι : Type u_5} {α : Type u_6} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤ - Finset.max_eq_sup_coe 📋 Mathlib.Data.Finset.Max
{α : Type u_1} [LinearOrder α] {s : Finset α} : s.max = s.sup WithBot.some - Finset.max_eq_sup_withBot 📋 Mathlib.Data.Finset.Max
{α : Type u_1} [LinearOrder α] (s : Finset α) : s.max = s.sup WithBot.some - Finset.sup_eq_biUnion 📋 Mathlib.Data.Finset.Lattice.Union
{α : Type u_7} {β : Type u_8} [DecidableEq β] (s : Finset α) (t : α → Finset β) : s.sup t = s.biUnion t - Finset.sup_biUnion 📋 Mathlib.Data.Finset.Lattice.Union
{α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : β → α} [SemilatticeSup α] [OrderBot α] [DecidableEq β] (s : Finset γ) (t : γ → Finset β) : (s.biUnion t).sup f = s.sup fun x => (t x).sup f - Finset.powersetCard_sup 📋 Mathlib.Data.Finset.Powerset
{α : Type u_1} [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) : (Finset.powersetCard n.succ u).sup id = u - Finset.sup_univ_eq_ciSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Finset
{ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] [Fintype ι] (f : ι → α) : Finset.univ.sup f = ⨆ i, f i - ciSup_eq_ciSup_finset 📋 Mathlib.Order.ConditionallyCompleteLattice.Finset
{ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] [OrderBot α] [Nonempty ι] {a : ι → α} (ha : BddAbove (Set.range a)) : ⨆ i, a i = ⨆ F, F.sup a - Finset.sup_eq_ciSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Finset
{ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] (s : Finset ι) (f : ι → α) : s.sup f = ⨆ x ∈ s, f x - Finset.sup_sigma 📋 Mathlib.Data.Finset.Sigma
{ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α i → β) [SemilatticeSup β] [OrderBot β] : (s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩ - Finset.sup_preimage_self 📋 Mathlib.Data.Finset.Preimage
{α : Type u_1} {β : Type u_2} [Nonempty α] [SemilatticeSup β] [OrderBot β] {s : Finset β} {f : α → β} (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) : (s.preimage f ⋯).sup f = s.sup id - Finset.sup_preimage_val_id 📋 Mathlib.Data.Finset.Preimage
{α : Type u} [Lattice α] [OrderBot α] {P : α → Prop} (Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)) (Pbot : P ⊥) {t : Finset α} (ht : ∀ x ∈ t, P x) : (t.preimage Subtype.val ⋯).sup id = ⟨t.sup id, ⋯⟩ - Finset.sup_Iic 📋 Mathlib.Order.Interval.Finset.Basic
{α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] (a : α) : (Finset.Iic a).sup id = a - Finset.sup_Iic_of_monotone 📋 Mathlib.Order.Interval.Finset.Basic
{α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] {β : Type u_3} [SemilatticeSup β] [OrderBot β] {f : α → β} (hf : Monotone f) : (Finset.Iic a).sup f = f a - Finset.subset_Iic_sup_id 📋 Mathlib.Order.Interval.Finset.Basic
{α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] (s : Finset α) : s ⊆ Finset.Iic (s.sup id) - Finset.image_subset_Iic_sup 📋 Mathlib.Order.Interval.Finset.Basic
{ι : Type u_1} {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] [DecidableEq α] (f : ι → α) (s : Finset ι) : Finset.image f s ⊆ Finset.Iic (s.sup f) - Finset.isPWO_sup 📋 Mathlib.Order.WellFoundedSet
{ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ι → Set α} : (s.sup f).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO - Finset.partiallyWellOrderedOn_sup 📋 Mathlib.Order.WellFoundedSet
{ι : Type u_1} {α : Type u_2} {r : α → α → Prop} (s : Finset ι) {f : ι → Set α} : (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r - Finset.isWF_sup 📋 Mathlib.Order.WellFoundedSet
{ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ι → Set α} : (s.sup f).IsWF ↔ ∀ i ∈ s, (f i).IsWF - Finset.wellFoundedOn_sup 📋 Mathlib.Order.WellFoundedSet
{ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α} : (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r - AddSubgroup.FG.finset_sup 📋 Mathlib.GroupTheory.Finiteness
{G : Type u_3} [AddGroup G] {ι : Type u_5} (s : Finset ι) (P : ι → AddSubgroup G) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG - Subgroup.FG.finset_sup 📋 Mathlib.GroupTheory.Finiteness
{G : Type u_3} [Group G] {ι : Type u_5} (s : Finset ι) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG - AddSubmonoid.FG.finset_sup 📋 Mathlib.GroupTheory.Finiteness
{M : Type u_1} [AddMonoid M] {ι : Type u_3} (s : Finset ι) (P : ι → AddSubmonoid M) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG - Submonoid.FG.finset_sup 📋 Mathlib.GroupTheory.Finiteness
{M : Type u_1} [Monoid M] {ι : Type u_3} (s : Finset ι) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG - Finset.sup_product_left 📋 Mathlib.Data.Finset.Lattice.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f (i, i') - Finset.sup_product_right 📋 Mathlib.Data.Finset.Lattice.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f (i, i') - Finset.sup_inf_sup 📋 Mathlib.Data.Finset.Lattice.Prod
{α : Type u_1} {ι : Type u_4} {κ : Type u_5} [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 - Finset.sup_prodMap 📋 Mathlib.Data.Finset.Lattice.Prod
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} {β : Type u_9} [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) - SupClosed.finsetSup_mem 📋 Mathlib.Order.SupClosed
{α : Type u_3} [SemilatticeSup α] {ι : Type u_5} {f : ι → α} {s : Set α} {t : Finset ι} [OrderBot α] (hs : SupClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s - Finset.supIndep_iff_disjoint_erase 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} [DecidableEq ι] : s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f) - Finset.SupIndep.insert 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] [DecidableEq ι] {i : ι} {s : Finset ι} {f : ι → α} (hs : s.SupIndep f) (h : Disjoint (f i) (s.sup f)) : (insert i s).SupIndep f - Finset.SupIndep.biUnion 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α} (hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) : (s.biUnion g).SupIndep f - Finset.SupIndep.union 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] [DecidableEq ι] {s t : Finset ι} {f : ι → α} (hs : s.SupIndep f) (ht : t.SupIndep f) (h : Disjoint (s.sup f) (t.sup f)) : (s ∪ t).SupIndep f - Finset.supIndep_product_iff 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} : (s.product t).SupIndep f ↔ (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i') - Finset.SupIndep.sup 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α} (hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) : (s.sup g).SupIndep f - Finset.SupIndep.product 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} (hs : s.SupIndep fun i => t.sup fun i' => f (i, i')) (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) : (s ×ˢ t).SupIndep f - Finset.SupIndep.disjoint_sup_sup 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} {u v : Finset ι} (hs : s.SupIndep f) (hu : u ⊆ s) (hv : v ⊆ s) (huv : Disjoint u v) : Disjoint (u.sup f) (v.sup f) - Finset.SupIndep.sigma 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] {β : ι → Type u_5} {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma β → α} (hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩) (hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩) : (s.sigma g).SupIndep f - Finset.supIndep_sigma_iff' 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] {β : ι → Type u_5} {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma β → α} : (s.sigma g).SupIndep f ↔ (s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩) ∧ ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩ - Finset.SupIndep.le_sup_iff 📋 Mathlib.Order.SupIndep
{α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s t : Finset ι} {f : ι → α} {i : ι} (hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ (i : ι), f i ≠ ⊥) : f i ≤ t.sup f ↔ i ∈ t - CompleteLattice.isCompactElement_finsetSup 📋 Mathlib.Order.CompactlyGenerated.Basic
{α : Type u_3} {β : Type u_4} [CompleteLattice α] {f : β → α} (s : Finset β) (h : ∀ x ∈ s, IsCompactElement (f x)) : IsCompactElement (s.sup f) - CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup 📋 Mathlib.Order.CompactlyGenerated.Basic
{α : Type u} [CompleteLattice α] (k : α) : IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s - CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup 📋 Mathlib.Order.CompactlyGenerated.Basic
(α : Type u_2) [CompleteLattice α] (k : α) : IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id - inf_sSup_eq_iSup_inf_sup_finset 📋 Mathlib.Order.CompactlyGenerated.Basic
{α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} : a ⊓ sSup s = ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id - Multiset.sup_powerset_len 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{α : Type u_2} [DecidableEq α] (x : Multiset α) : ((Finset.range (x.card + 1)).sup fun k => Multiset.powersetCard k x) = x.powerset - Multiset.finsetSum_eq_sup_iff_disjoint 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{α : Type u_2} {β : Type u_3} [DecidableEq α] {i : Finset β} {f : β → Multiset α} : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y) - Multiset.finset_sum_eq_sup_iff_disjoint 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{α : Type u_2} {β : Type u_3} [DecidableEq α] {i : Finset β} {f : β → Multiset α} : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y) - Finset.apply_sup_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] [AddCommMonoid β] [Preorder β] [AddLeftMono β] {f : α → β} (zero : f ⊥ = 0) (ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t) {s : ι → α} (t : Finset ι) : f (t.sup s) ≤ ∑ i ∈ t, f (s i) - Finset.sup_fin_univ 📋 Mathlib.Data.Fintype.Fin
{α : Type u_1} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : ℕ → α) : (Finset.univ.sup fun n_1 => f ↑n_1) = (Finset.range n).sup f - partialSups_eq_sup_range 📋 Mathlib.Order.PartialSups
{α : Type u_1} [SemilatticeSup α] [OrderBot α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = (Finset.range (n + 1)).sup f - disjointed_apply 📋 Mathlib.Order.Disjointed
{α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) : disjointed f i = f i \ (Finset.Iio i).sup f - Fintype.sup_disjointed 📋 Mathlib.Order.Disjointed
{α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [PartialOrder ι] [LocallyFiniteOrderBot ι] [Fintype ι] (f : ι → α) : Finset.univ.sup (disjointed f) = Finset.univ.sup f - Fintype.exists_disjointed_le 📋 Mathlib.Order.Disjointed
{α : Type u_1} [GeneralizedBooleanAlgebra α] {ι : Type u_3} [Fintype ι] (f : ι → α) : ∃ g ≤ f, Finset.univ.sup g = Finset.univ.sup f ∧ Pairwise (Function.onFun Disjoint g) - sup_Ioc_disjointed_of_monotone 📋 Mathlib.Order.Disjointed
{α : Type u_1} [GeneralizedBooleanAlgebra α] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] {f : ι → α} (hf : Monotone f) {m n : ι} (hm : n ≤ m) : (Finset.Ioc n m).sup (disjointed f) = f m \ f n - Submodule.fg_finset_sup 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) : (s.sup N).FG - Submodule.finite_finset_sup 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_2} {V : Type u_3} [Ring R] [AddCommGroup V] [Module R V] {ι : Type u_1} (s : Finset ι) (S : ι → Submodule R V) [∀ (i : ι), Module.Finite R ↥(S i)] : Module.Finite R ↥(s.sup S) - Finset.sup_image₂_left 📋 Mathlib.Data.Finset.NAry
{α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} (s : Finset α) (t : Finset β) [SemilatticeSup δ] [OrderBot δ] (g : γ → δ) : (Finset.image₂ f s t).sup g = s.sup fun x => t.sup fun x_1 => g (f x x_1) - Finset.sup_image₂_right 📋 Mathlib.Data.Finset.NAry
{α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} (s : Finset α) (t : Finset β) [SemilatticeSup δ] [OrderBot δ] (g : γ → δ) : (Finset.image₂ f s t).sup g = t.sup fun y => s.sup fun x => g (f x y) - Finset.sup_image₂_le 📋 Mathlib.Data.Finset.NAry
{α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeSup δ] [OrderBot δ] {g : γ → δ} {a : δ} : (Finset.image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a - Finset.sup_one 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [One α] [SemilatticeSup β] [OrderBot β] (f : α → β) : Finset.sup 1 f = f 1 - Finset.sup_zero 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [Zero α] [SemilatticeSup β] [OrderBot β] (f : α → β) : Finset.sup 0 f = f 0 - Finset.sup_inv 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Inv α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : s⁻¹.sup f = s.sup fun x => f x⁻¹ - Finset.sup_neg 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Neg α] [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : (-s).sup f = s.sup fun x => f (-x) - Finset.sup_add_left 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [Add α] {β : Type u_4} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s + t).sup f = s.sup fun x => t.sup fun x_1 => f (x + x_1) - Finset.sup_add_right 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [Add α] {β : Type u_4} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s + t).sup f = t.sup fun y => s.sup fun x => f (x + y) - Finset.sup_div_left 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s / t).sup f = s.sup fun x => t.sup fun x_1 => f (x / x_1) - Finset.sup_div_right 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s / t).sup f = t.sup fun y => s.sup fun x => f (x / y) - Finset.sup_mul_left 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_4} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s * t).sup f = s.sup fun x => t.sup fun x_1 => f (x * x_1) - Finset.sup_mul_right 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_4} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s * t).sup f = t.sup fun y => s.sup fun x => f (x * y) - Finset.sup_sub_left 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s - t).sup f = s.sup fun x => t.sup fun x_1 => f (x - x_1) - Finset.sup_sub_right 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : (s - t).sup f = t.sup fun y => s.sup fun x => f (x - y) - Finset.sup_add_le 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [Add α] {β : Type u_4} [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s + t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x + y) ≤ a - Finset.sup_div_le 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Div α] [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s / t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x / y) ≤ a - Finset.sup_mul_le 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [Mul α] {β : Type u_4} [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s * t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a - Finset.sup_sub_le 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [Sub α] [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} : (s - t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x - y) ≤ a - Finset.sup_univ_eq_iSup 📋 Mathlib.Data.Fintype.Lattice
{α : Type u_2} {β : Type u_3} [Fintype α] [CompleteLattice β] (f : α → β) : Finset.univ.sup f = iSup f - Ideal.sum_eq_sup 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Ideal R) : s.sum f = s.sup f - Finset.add_sup 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup f = s.sup fun i => a + f i - Finset.sup_add 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : s.sup f + a = s.sup fun i => f i + a - Finset.sup_add_sup 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} {t : Finset κ} [OrderBot M] (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) : s.sup f + t.sup g = (s ×ˢ t).sup fun ij => f ij.1 + g ij.2 - Submodule.finiteDimensional_finset_sup 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} (s : Finset ι) (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K ↥(S i)] : FiniteDimensional K ↥(s.sup S) - sup_eq_of_isMaxOn 📋 Mathlib.Order.Filter.Extr
{α : Type u} {β : Type v} [SemilatticeSup β] [OrderBot β] {D : α → β} {s : Finset α} {a : α} (hmem : a ∈ s) (hmax : IsMaxOn D (↑s) a) : s.sup D = D a - sup_eq_of_max 📋 Mathlib.Order.Filter.Extr
{α : Type u} {β : Type v} [SemilatticeSup β] [OrderBot β] {D : α → β} {s : Finset α} [Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : Function.invFun D b ∈ s) (hmax : ∀ a ∈ s, D a ≤ b) : s.sup D = b - AddMonoidAlgebra.supDegree_sum_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} : AddMonoidAlgebra.supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i => AddMonoidAlgebra.supDegree D (f i) - AddMonoidAlgebra.sup_support_add_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] (degb : A → B) (f g : AddMonoidAlgebra R A) : (f + g).coeff.support.sup degb ≤ f.coeff.support.sup degb ⊔ g.coeff.support.sup degb - AddMonoidAlgebra.sup_support_coeff_add_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] (degb : A → B) (f g : AddMonoidAlgebra R A) : (f + g).coeff.support.sup degb ≤ f.coeff.support.sup degb ⊔ g.coeff.support.sup degb - AddMonoidAlgebra.sup_support_coeff_mul_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] [Add A] [Add B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (f g : AddMonoidAlgebra R A) : (f * g).coeff.support.sup degb ≤ f.coeff.support.sup degb + g.coeff.support.sup degb - AddMonoidAlgebra.sup_support_mul_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] [Add A] [Add B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (f g : AddMonoidAlgebra R A) : (f * g).coeff.support.sup degb ≤ f.coeff.support.sup degb + g.coeff.support.sup degb - AddMonoidAlgebra.sup_support_list_prod_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] [AddMonoid A] [AddMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (l : List (AddMonoidAlgebra R A)) : l.prod.coeff.support.sup degb ≤ (List.map (fun f => f.coeff.support.sup degb) l).sum - AddMonoidAlgebra.sup_support_pow_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] [AddMonoid A] [AddMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (n : ℕ) (f : AddMonoidAlgebra R A) : (f ^ n).coeff.support.sup degb ≤ n • f.coeff.support.sup degb - AddMonoidAlgebra.sup_support_coeff_finsetProd_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} {ι : Type u_6} [SemilatticeSup B] [OrderBot B] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (s : Finset ι) (f : ι → AddMonoidAlgebra R A) : (∏ i ∈ s, f i).coeff.support.sup degb ≤ ∑ i ∈ s, (f i).coeff.support.sup degb - AddMonoidAlgebra.sup_support_finsetProd_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} {ι : Type u_6} [SemilatticeSup B] [OrderBot B] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (s : Finset ι) (f : ι → AddMonoidAlgebra R A) : (∏ i ∈ s, f i).coeff.support.sup degb ≤ ∑ i ∈ s, (f i).coeff.support.sup degb - AddMonoidAlgebra.sup_support_finset_prod_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} {ι : Type u_6} [SemilatticeSup B] [OrderBot B] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (s : Finset ι) (f : ι → AddMonoidAlgebra R A) : (∏ i ∈ s, f i).coeff.support.sup degb ≤ ∑ i ∈ s, (f i).coeff.support.sup degb - AddMonoidAlgebra.sup_support_coeff_multisetProd_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (m : Multiset (AddMonoidAlgebra R A)) : m.prod.coeff.support.sup degb ≤ (Multiset.map (fun f => f.coeff.support.sup degb) m).sum - AddMonoidAlgebra.sup_support_multiset_prod_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (m : Multiset (AddMonoidAlgebra R A)) : m.prod.coeff.support.sup degb ≤ (Multiset.map (fun f => f.coeff.support.sup degb) m).sum - Polynomial.degree_sum_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
{R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree - MvPolynomial.totalDegree_finsetSum 📋 Mathlib.Algebra.MvPolynomial.Degrees
{R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R) : (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree - MvPolynomial.totalDegree_finset_sum 📋 Mathlib.Algebra.MvPolynomial.Degrees
{R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R) : (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree - MvPolynomial.degreeOf_eq_sup 📋 Mathlib.Algebra.MvPolynomial.Degrees
{R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) (f : MvPolynomial σ R) : MvPolynomial.degreeOf n f = f.support.sup fun m => m n - MvPolynomial.degreeOf_sum_le 📋 Mathlib.Algebra.MvPolynomial.Degrees
{R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) : MvPolynomial.degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j => MvPolynomial.degreeOf i (f j) - MvPolynomial.degrees_sum_le 📋 Mathlib.Algebra.MvPolynomial.Degrees
{R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq σ] (s : Finset ι) (f : ι → MvPolynomial σ R) : (∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees - MvPolynomial.totalDegree_eq 📋 Mathlib.Algebra.MvPolynomial.Degrees
{R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : p.totalDegree = p.support.sup fun m => (Finsupp.toMultiset m).card - MvPolynomial.degrees_def 📋 Mathlib.Algebra.MvPolynomial.Degrees
{R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) : p.degrees = p.support.sup fun s => Finsupp.toMultiset s - Polynomial.natDegree_sum_eq_of_disjoint 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
{R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.natDegree ∘ f))) : (s.sum f).natDegree = s.sup fun i => (f i).natDegree - Polynomial.degree_sum_eq_of_disjoint 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
{R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.degree ∘ f))) : (s.sum f).degree = s.sup fun i => (f i).degree - Polynomial.natDegree_sum_eq_of_linearIndepOn 📋 Mathlib.Algebra.Polynomial.BigOperators
{R : Type u} {ι : Type w} (s : Finset ι) [CommRing R] {A : Type u_1} [CommRing A] [Algebra R A] {f : ι → Polynomial R} {v : ι → A} (h : LinearIndepOn R v ↑s) : (∑ i ∈ s, v i • Polynomial.map (algebraMap R A) (f i)).natDegree = s.sup fun i => (f i).natDegree - Polynomial.degree_sum_eq_of_linearIndepOn 📋 Mathlib.Algebra.Polynomial.BigOperators
{R : Type u} {ι : Type w} (s : Finset ι) [CommRing R] {A : Type u_1} [CommRing A] [Algebra R A] {f : ι → Polynomial R} {v : ι → A} (h : LinearIndepOn R v ↑s) : (∑ i ∈ s, v i • Polynomial.map (algebraMap R A) (f i)).degree = s.sup fun i => (f i).degree - Nat.sup_divisors_id 📋 Mathlib.NumberTheory.Divisors
(n : ℕ) : n.divisors.sup id = n - Finset.sym_succ 📋 Mathlib.Data.Finset.Sym
{α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} : s.sym (n + 1) = s.sup fun a => Finset.image (Sym.cons a) (s.sym n) - AddSubgroup.finsetSup_zmultiples 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
{G : Type u_1} [AddGroup G] (s : Finset G) : s.sup AddSubgroup.zmultiples = AddSubgroup.closure ↑s - Subgroup.finsetSup_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
{G : Type u_1} [Group G] (s : Finset G) : s.sup Subgroup.zpowers = Subgroup.closure ↑s
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.You can filter for definitions vs theorems: Using
⊢ (_ : Type _)finds all definitions which provide data while⊢ (_ : Prop)finds all theorems (and definitions of proofs).
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision 69fae59