Package real-thm: real-thm

Information

namereal-thm
version1.7
descriptionreal-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-09-21
showData.Bool

Files

Theorem

P.
    (x. P x) (M. x. P x Number.Real.≤ x M)
    M.
      (x. P x Number.Real.≤ x M)
      M'. (x. P x Number.Real.≤ x M') Number.Real.≤ M M'

Input Type Operators

Input Constants

Assumptions

T

F p. p

x. ¬Set.∈ x Set.∅

(¬) = λp. p F

() = λp. p = λx. T

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f T T

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

s t. s = t x. Set.∈ x s Set.∈ x t

(t. ¬¬t t) (¬T F) (¬F T)

p x. Set.∈ x { y. y | p y } p x

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

s.
    ¬(s = Set.∅) (m. x. Set.∈ x s Number.Real.≤ x m)
    (x. Set.∈ x s Number.Real.≤ x (Number.Real.sup s))
    m.
      (x. Set.∈ x s Number.Real.≤ x m)
      Number.Real.≤ (Number.Real.sup s) m