Zulip Chat Archive
Stream: maths
Topic: argmin
Jakob von Raumer (Nov 25 2022 at 11:14):
I can't seem to find an argmin for set, is it called differently?
Yaël Dillies (Nov 25 2022 at 11:51):
I think you're just meant to use the preimage of Sup
Oliver Nash (Nov 25 2022 at 13:15):
Does docs#function.argmin_on help?
Jakob von Raumer (Nov 30 2022 at 08:50):
Oliver Nash said:
Does docs#function.argmin_on help?
Yes, thanks, that's what I was looking for, at the wrong end of mathlib
Last updated: Dec 20 2023 at 11:08 UTC