module module

`IndisputableMonolith.RRF.Theorems.MonotoneArgmin`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RRF.Theorems module_import

declarations in this module (8)

def isArgmin L27
theorem argmin_comp_strictMono L35
theorem argmin_of_comp_strictMono L43
theorem strictOrder_comp_strictMono L56
theorem weakOrder_comp_mono L63
theorem argmin_equiv_strictMono L70
theorem argmin_add_const L75
theorem argmin_mul_pos L86