Extensions to Finset

The intention is to upstream these to mathlib.

noncomputable def Finset.argmin {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] : α

Equations

• S.argmin hS f = ⋯.choose

noncomputable def Finset.argmin_spec {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] : S.argmin hS f ∈ S ∧ S.inf' hS f = f (S.argmin hS f)

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.argmin_le {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] (a : α) (ha : a ∈ S) : f (S.argmin hS f) ≤ f a

@[simp]

theorem Finset.argmin_mem {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] : S.argmin hS f ∈ S

@[simp]

theorem Finset.toFinset_argmin_mem {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] (S : Set α) [Fintype ↑S] (hS : S.toFinset.Nonempty) : S.toFinset.argmin hS f ∈ S

noncomputable def Finset.argmax {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] : α

Equations

• S.argmax hS f = ⋯.choose

noncomputable def Finset.argmax_spec {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] : S.argmax hS f ∈ S ∧ S.sup' hS f = f (S.argmax hS f)

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.argmax_le {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] (a : α) (ha : a ∈ S) : f a ≤ f (S.argmax hS f)

@[simp]

theorem Finset.argmax_mem {α : Type u_1} {β : Type u_2} (S : Finset α) (hS : S.Nonempty) (f : α → β) [LinearOrder β] : S.argmax hS f ∈ S

@[simp]

theorem Finset.toFinset_argmax_mem {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] (S : Set α) [Fintype ↑S] (hS : S.toFinset.Nonempty) : S.toFinset.argmax hS f ∈ S