|
Table data: (P,Q)
such that (P)⟹(Q)
Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| FallingFactorial | (z)k | Falling factorial |
| CC | C | Complex numbers |
| ZZGreaterEqual | Z≥n | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("3c2469"),
SymbolDefinition(FallingFactorial, FallingFactorial(z, k), "Falling factorial"),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(z, CC), Element(k, ZZGreaterEqual(0))), Element(FallingFactorial(z, k), CC)))))