1.5. ForMathlib.MeasureTheory.Order.MeasurableArg🔗

Argmax and argmin functions on finite sets

We prove in particular that those functions are measurable.

Module LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg contains 17 exposed declarations.

• Function.maxDefinition · 0 deps
• Function.minDefinition · 0 deps
• Function.le_maxLemma · 1 deps
• Function.min_leLemma · 1 deps
• exists_argmaxLemma · 1 deps
• exists_argminLemma · 1 deps
• argmaxDefinition · 2 deps
• argminDefinition · 2 deps
• argmax_specLemma · 3 deps
• argmin_specLemma · 3 deps
• isMaxOn_argmaxLemma · 3 deps
• isMinOn_argminLemma · 3 deps
• measurable_maxLemma · 1 deps
• measurable_minLemma · 1 deps
• measurable_argmaxLemma · 3 deps
• measurable_argminLemma · 3 deps
• neg_max_eq_min_negLemma · 2 deps