Package real-thm: Properties of the real numbers

Information

namereal-thm
version1.44
descriptionProperties of the real numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2014-06-12
requiresbool
real-def
set
showData.Bool
Number.Real
Set

Files

Theorem

p.
    (x. p x) (m. x. p x x m)
    s. (x. p x x s) m. (x. p x x m) s m

External Type Operators

External Constants

Assumptions

t. (x. t) t

() = λp. p = λx.

t. t t

() = λp q. p q p

s. (x. x s) ¬(s = )

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

() = λp. q. (x. p x q) q

p x. x { y. y | p y } p x

s x. ¬(s = ) (m. x. x s x m) x s x sup s

s m.
    ¬(s = ) (m. x. x s x m) (x. x s x m) sup s m