The following table lists conditions such that Pow(a, b) is defined in Fungrim.
|
Table data:
such that
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Pow | Power | |
CC | Complex numbers | |
Infinity | Positive infinity | |
UnsignedInfinity | Unsigned infinity | |
ZZLessEqual | Integers less than or equal to n | |
ZZGreaterEqual | Integers greater than or equal to n | |
Rational numbers | ||
ZZ | Integers |
Source code for this entry:
Entry(ID("ef9f8a"), SymbolDefinition(Pow, Pow(a, b), "Power"), Description(""), Description("The following table lists conditions such that", SourceForm(Pow(a, b)), "is defined in Fungrim."), Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(And(Element(a, SetMinus(CC, 0)), Element(b, CC)), Element(Pow(a, b), CC)), Tuple(And(Element(a, CC), Element(b, Set(0))), Element(Pow(a, b), Set(1))), TableSection("Infinities"), Tuple(And(Element(a, Set(Infinity, Neg(Infinity), UnsignedInfinity)), Element(b, ZZLessEqual(-1))), Element(Pow(a, b), Set(0))), TableSection("General domains"), Tuple(And(Element(a, R), Element(R, Rings), Element(b, ZZGreaterEqual(0))), Element(Pow(a, b), R)), Tuple(And(Element(a, SetMinus(K, Set(0))), Element(K, Fields), SubsetEqual(QQ, K), Element(b, ZZ)), Element(Pow(a, b), R)))))