Package real-thm: Properties of the real numbers
Information
| name | real-thm |
| version | 1.32 |
| description | Properties of the real numbers |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2012-06-08 |
| requires | bool real-def set |
| show | Data.Bool Number.Real Set |
Files
- Package tarball real-thm-1.32.tgz
- Theory file real-thm.thy (included in the package tarball)
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
Input Type Operators
- →
- bool
- Number
- Real
- real
- Real
- Set
- set
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- ⊤
- Bool
- Number
- Real
- ≤
- sup
- Real
- Set
- ∅
- fromPredicate
- ∈
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