Как написать ARG_MIN в Isabelle

#isabelle #isabelle Вопрос: Я пытаюсь переписать следующее arg_min выражение в Isabelle (2020) в более удобный синтаксис ARG_MIN. lemma "1 = arg_min (λ(x::int). x*x) ((<) 0)" Что у меня есть до…