Package real-thm: real-thm

Information

name	real-thm
version	1.7
description	real-thm
author	Joe Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2011-09-21
show	Data.Bool

Files

Package tarball real-thm-1.7.tgz
Theory file real-thm.thy (included in the package tarball)

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

→
bool
Number
- Real
  - Number.Real.real
Set
- Set.set

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ¬
  - F
  - T
Number
- Real
  - Number.Real.≤
  - Number.Real.sup
Set
- Set.∅
- Set.fromPredicate
- Set.∈

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