Theory "HO_arith_utils"

Parents     indexedLists   patternMatches

Theorems

general_theorem
|- ∀P f l.
     (∀p. P p ∧ f p > l ⇒ ∃p'. P p' ∧ f p' < f p) ⇒
     ∀p. P p ⇒ ∃p'. P p' ∧ f p' ≤ l
general_theorem'
|- ∀P f l prob.
     (∀p. P (prob,p) ∧ f p > l ⇒ ∃p'. P (prob,p') ∧ f p' < f p) ⇒
     ∀p. P (prob,p) ⇒ ∃p'. P (prob,p') ∧ f p' ≤ l