|
Table data:
such that
Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Sign | Sign function | |
| RR | Real numbers | |
| CC | Complex numbers | |
| UnitCircle | Unit circle | |
| Infinity | Positive infinity |
Source code for this entry:
Entry(ID("5e639e"),
SymbolDefinition(Sign, Sign(z), "Sign function"),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Sign(z), Set(-1, 0, 1))), Tuple(Element(z, SetMinus(CC, Set(0))), Element(Sign(z), UnitCircle)), Tuple(Element(z, Set(Infinity)), Element(Sign(z), Set(1))), Tuple(Element(z, Set(Neg(Infinity))), Element(Sign(z), Set(-1))))))