Package axiom: Standard axioms

Information

nameaxiom
version1.12
descriptionStandard axioms
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
showData.Bool
Function

Files

Theorems

t. (λx. t x) = t

f. injective f ¬surjective f

p x. p x p ((select) p)

External Type Operators

External Constants

Assumptions

AXIOM OF EXTENSIONALITY

AXIOM OF CHOICE

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