Skip to content

Commit c7a2a0d

Browse files
Update LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
1 parent 42a054f commit c7a2a0d

1 file changed

Lines changed: 3 additions & 1 deletion

File tree

‎LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,9 @@ public import Mathlib.CategoryTheory.Countable
1010
public import Mathlib.MeasureTheory.Constructions.Polish.Basic
1111
public import Mathlib.Order.CompletePartialOrder
1212

13-
/-! # Measurable argmax and argmin functions
13+
/-! # Argmax and argmin functions on finite sets
14+
15+
We prove in particular that those functions are measurable.
1416
1517
-/
1618

0 commit comments

Comments
 (0)