Down The Type Hole Pasting Service

Paste "Untitled paste" by Anonymous

Time of creation: 2017-07-17 13:13:22.502061 UTC

definition arg_min_set :: "('a ⇒ 'b::ord) ⇒ 'a set ⇒ 'a set"  
  where
    "arg_min_set f S = {x. is_arg_min f (λx. x∈S) x}"

definition arg_max_set :: "('a ⇒ 'b::ord) ⇒ 'a set ⇒ 'a set"  
  where
    "arg_max_set f S = {x. is_arg_max f (λx. x∈S) x}"