Down The Type Hole Pasting Service

Paste "Untitled paste" by Anonymous

Time of creation: 2017-07-17 13:21:22.418249 UTC

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}"

lemma "arg_max_set f S = {x ∈ S . ∀y ∈ S. f x ≥ f y}"