Package axiom-infinity: axiom-infinity

Information

Files

• Package tarball axiom-infinity-1.0.tgz
• Theory file axiom-infinity.thy (included in the package tarball)

Theorem

⊦ ∃f. Function.injective f ∧ ¬Function.surjective f

Input Type Operators

• →
• bool
• ind

Input Constants

• Data
  • Bool
    • ∧
    • ∃
    • ~
• Function
  • Function.injective
  • Function.surjective

Assumption

⊦ ∃f. Function.injective f ∧ ¬Function.surjective f