Package axiom-infinity: Axiom of Infinity

Information

nameaxiom-infinity
version1.8
descriptionAxiom of Infinity
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2013-12-10
requiresbool
function
showData.Bool
Function

Files

Theorem

f. injective f ¬surjective f

External Type Operators

External Constants

Assumptions

AXIOM OF INFINITY

p. p

(¬) = λp. p

(λp. p) = λp. p

() = λp. p = λx.

() = λp q. p q p

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

f. surjective f y. x. y = f x

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

f. injective f x1 x2. f x1 = f x2 x1 = x2