|
Table data: (P,Q)
such that (P)⟹(Q)
Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Sign | sgn(z) | Sign function |
| RR | R | Real numbers |
| CC | C | Complex numbers |
| UnitCircle | T | 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))))))