|
Table data: (P,Q)
such that (P)⟹(Q)
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
BernoulliPolynomial | Bn(z) | Bernoulli polynomial |
ZZGreaterEqual | Z≥n | Integers greater than or equal to n |
RR | R | Real numbers |
CC | C | Complex numbers |
Q | Rational numbers |
Source code for this entry:
Entry(ID("1f88a4"), SymbolDefinition(BernoulliPolynomial, BernoulliPolynomial(n, z), "Bernoulli polynomial"), Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(n, ZZGreaterEqual(0)), Element(z, RR)), Element(BernoulliPolynomial(n, z), RR)), Tuple(And(Element(n, ZZGreaterEqual(0)), Element(z, CC)), Element(BernoulliPolynomial(n, z), CC)), Tuple(And(Element(n, ZZGreaterEqual(0)), Element(z, R), Element(R, Rings), SubsetEqual(QQ, R)), Element(BernoulliPolynomial(n, z), R)))))