Theorems · Definition · order theory

Function.argmin

{α : Type u_1} → {β : Type u_2} → (α → β) → [inst : LT β] → [WellFoundedLT β] → [Nonempty α] → α

Given a function f : α → β where β carries a well-founded <, this is an element of α whose image under f is minimal in the sense of Function.not_lt_argmin. See also Set.Finite.exists_minimalFor and related lemmas for the case when α is finite.

Defined in

Mathlib.Order.WellFounded

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LTWellFoundedLTNonempty