Symbol: Sign — sgn ( z ) \operatorname{sgn}\!\left(z\right) s g n ( z ) — Sign function
Domain Codomain z ∈ R z \in \mathbb{R} z ∈ R sgn ( z ) ∈ { − 1 , 0 , 1 } \operatorname{sgn}\!\left(z\right) \in \left\{-1, 0, 1\right\} s g n ( z ) ∈ { − 1 , 0 , 1 } z ∈ C ∖ { 0 } z \in \mathbb{C} \setminus \left\{0\right\} z ∈ C ∖ { 0 } sgn ( z ) ∈ T \operatorname{sgn}\!\left(z\right) \in \mathbb{T} s g n ( z ) ∈ T z ∈ { ∞ } z \in \left\{\infty\right\} z ∈ { ∞ } sgn ( z ) ∈ { 1 } \operatorname{sgn}\!\left(z\right) \in \left\{1\right\} s g n ( z ) ∈ { 1 } z ∈ { − ∞ } z \in \left\{-\infty\right\} z ∈ { − ∞ } sgn ( z ) ∈ { − 1 } \operatorname{sgn}\!\left(z\right) \in \left\{-1\right\} s g n ( z ) ∈ { − 1 }
Table data:
( P , Q ) \left(P, Q\right) ( P , Q )
such that
( P ) ⟹ ( Q ) \left(P\right) \implies \left(Q\right) ( P ) ⟹ ( Q ) Definitions:
Fungrim symbol Notation Short description Sign sgn ( z ) \operatorname{sgn}\!\left(z\right) s g n ( z ) Sign function RR R \mathbb{R} R Real numbers CC C \mathbb{C} C Complex numbers UnitCircle T \mathbb{T} T Unit circle Infinity ∞ \infty ∞ 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)))))) Symbol: Abs — ∣ z ∣ \left|z\right| ∣ z ∣ — Absolute value
Domain Codomain z ∈ R z \in \mathbb{R} z ∈ R ∣ z ∣ ∈ [ 0 , ∞ ) \left|z\right| \in \left[0, \infty\right) ∣ z ∣ ∈ [ 0 , ∞ ) z ∈ C z \in \mathbb{C} z ∈ C ∣ z ∣ ∈ [ 0 , ∞ ) \left|z\right| \in \left[0, \infty\right) ∣ z ∣ ∈ [ 0 , ∞ ) z ∈ { ∞ , − ∞ , ∞ ~ } z \in \left\{\infty, -\infty, {\tilde \infty}\right\} z ∈ { ∞ , − ∞ , ∞ ~ } ∣ z ∣ ∈ { ∞ } \left|z\right| \in \left\{\infty\right\} ∣ z ∣ ∈ { ∞ }
Table data:
( P , Q ) \left(P, Q\right) ( P , Q )
such that
( P ) ⟹ ( Q ) \left(P\right) \implies \left(Q\right) ( P ) ⟹ ( Q ) Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value RR R \mathbb{R} R Real numbers ClosedOpenInterval [ a , b ) \left[a, b\right) [ a , b ) Closed-open interval Infinity ∞ \infty ∞ Positive infinity CC C \mathbb{C} C Complex numbers UnsignedInfinity ∞ ~ {\tilde \infty} ∞ ~ Unsigned infinity
Source code for this entry:
Entry(ID("920cc8"),
SymbolDefinition(Abs, Abs(z), "Absolute value"),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Abs(z), ClosedOpenInterval(0, Infinity))), Tuple(Element(z, CC), Element(Abs(z), ClosedOpenInterval(0, Infinity))), Tuple(Element(z, Set(Infinity, Neg(Infinity), UnsignedInfinity)), Element(Abs(z), Set(Infinity)))))) Symbol: Arg — arg ( z ) \arg\!\left(z\right) arg ( z ) — Complex argument
Domain Codomain z ∈ R z \in \mathbb{R} z ∈ R arg ( z ) ∈ { 0 , π } \arg\!\left(z\right) \in \left\{0, \pi\right\} arg ( z ) ∈ { 0 , π } z ∈ C z \in \mathbb{C} z ∈ C arg ( z ) ∈ ( − π , π ] \arg\!\left(z\right) \in \left(-\pi, \pi\right] arg ( z ) ∈ ( − π , π ] z ∈ { ∞ } z \in \left\{\infty\right\} z ∈ { ∞ } arg ( z ) ∈ { 0 } \arg\!\left(z\right) \in \left\{0\right\} arg ( z ) ∈ { 0 } z ∈ { − ∞ } z \in \left\{-\infty\right\} z ∈ { − ∞ } arg ( z ) ∈ { π } \arg\!\left(z\right) \in \left\{\pi\right\} arg ( z ) ∈ { π }
Table data:
( P , Q ) \left(P, Q\right) ( P , Q )
such that
( P ) ⟹ ( Q ) \left(P\right) \implies \left(Q\right) ( P ) ⟹ ( Q ) Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument RR R \mathbb{R} R Real numbers ConstPi π \pi π The constant pi (3.14...) CC C \mathbb{C} C Complex numbers OpenClosedInterval ( a , b ] \left(a, b\right] ( a , b ] Open-closed interval Infinity ∞ \infty ∞ Positive infinity
Source code for this entry:
Entry(ID("b7d740"),
SymbolDefinition(Arg, Arg(z), "Complex argument"),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Arg(z), Set(0, ConstPi))), Tuple(Element(z, CC), Element(Arg(z), OpenClosedInterval(Neg(ConstPi), ConstPi))), Tuple(Element(z, Set(Infinity)), Element(Arg(z), Set(0))), Tuple(Element(z, Set(Neg(Infinity))), Element(Arg(z), Set(ConstPi)))))) Symbol: Re — Re ( z ) \operatorname{Re}\!\left(z\right) R e ( z ) — Real part
Domain Codomain z ∈ R z \in \mathbb{R} z ∈ R Re ( z ) ∈ R \operatorname{Re}\!\left(z\right) \in \mathbb{R} R e ( z ) ∈ R z ∈ C z \in \mathbb{C} z ∈ C Re ( z ) ∈ R \operatorname{Re}\!\left(z\right) \in \mathbb{R} R e ( z ) ∈ R
Table data:
( P , Q ) \left(P, Q\right) ( P , Q )
such that
( P ) ⟹ ( Q ) \left(P\right) \implies \left(Q\right) ( P ) ⟹ ( Q ) Definitions:
Fungrim symbol Notation Short description Re Re ( z ) \operatorname{Re}\!\left(z\right) R e ( z ) Real part RR R \mathbb{R} R Real numbers CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("f5e62c"),
SymbolDefinition(Re, Re(z), "Real part"),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Re(z), RR)), Tuple(Element(z, CC), Element(Re(z), RR))))) Symbol: Im — Im ( z ) \operatorname{Im}\!\left(z\right) I m ( z ) — Imaginary part
Domain Codomain z ∈ R z \in \mathbb{R} z ∈ R Im ( z ) ∈ { 0 } \operatorname{Im}\!\left(z\right) \in \left\{0\right\} I m ( z ) ∈ { 0 } z ∈ C z \in \mathbb{C} z ∈ C Im ( z ) ∈ R \operatorname{Im}\!\left(z\right) \in \mathbb{R} I m ( z ) ∈ R
Table data:
( P , Q ) \left(P, Q\right) ( P , Q )
such that
( P ) ⟹ ( Q ) \left(P\right) \implies \left(Q\right) ( P ) ⟹ ( Q ) Definitions:
Fungrim symbol Notation Short description Im Im ( z ) \operatorname{Im}\!\left(z\right) I m ( z ) Imaginary part RR R \mathbb{R} R Real numbers CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("9086c6"),
SymbolDefinition(Im, Im(z), "Imaginary part"),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Im(z), Set(0))), Tuple(Element(z, CC), Element(Im(z), RR))))) Symbol: Conjugate — z ‾ \overline{z} z — Complex conjugate
Domain Codomain z ∈ R z \in \mathbb{R} z ∈ R z ‾ ∈ R \overline{z} \in \mathbb{R} z ∈ R z ∈ C z \in \mathbb{C} z ∈ C z ‾ ∈ C \overline{z} \in \mathbb{C} z ∈ C
Table data:
( P , Q ) \left(P, Q\right) ( P , Q )
such that
( P ) ⟹ ( Q ) \left(P\right) \implies \left(Q\right) ( P ) ⟹ ( Q ) Definitions:
Fungrim symbol Notation Short description Conjugate z ‾ \overline{z} z Complex conjugate RR R \mathbb{R} R Real numbers CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("da5d5e"),
SymbolDefinition(Conjugate, Conjugate(z), "Complex conjugate"),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Conjugate(z), RR)), Tuple(Element(z, CC), Element(Conjugate(z), CC))))) sgn ( z ) = z ∣ z ∣ \operatorname{sgn}\!\left(z\right) = \frac{z}{\left|z\right|} s g n ( z ) = ∣ z ∣ z Assumptions: z ∈ C ∖ { 0 } z \in \mathbb{C} \setminus \left\{0\right\} z ∈ C ∖ { 0 } TeX:
\operatorname{sgn}\!\left(z\right) = \frac{z}{\left|z\right|}
z \in \mathbb{C} \setminus \left\{0\right\} Definitions:
Fungrim symbol Notation Short description Sign sgn ( z ) \operatorname{sgn}\!\left(z\right) s g n ( z ) Sign function Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("26565c"),
Formula(Equal(Sign(z), Div(z, Abs(z)))),
Variables(z),
Assumptions(Element(z, SetMinus(CC, Set(0))))) ∣ x + y i ∣ = x 2 + y 2 \left|x + y i\right| = \sqrt{{x}^{2} + {y}^{2}} ∣ x + y i ∣ = x 2 + y 2 Assumptions: x ∈ R and y ∈ R x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} x ∈ R a n d y ∈ R TeX:
\left|x + y i\right| = \sqrt{{x}^{2} + {y}^{2}}
x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value ConstI i i i Imaginary unit Sqrt z \sqrt{z} z Principal square root Pow a b {a}^{b} a b Power RR R \mathbb{R} R Real numbers
Source code for this entry:
Entry(ID("4f0049"),
Formula(Equal(Abs(Add(x, Mul(y, ConstI))), Sqrt(Add(Pow(x, 2), Pow(y, 2))))),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR)))) arg ( x + y i ) = atan2 ( y , x ) \arg\!\left(x + y i\right) = \operatorname{atan2}\!\left(y, x\right) arg ( x + y i ) = a t a n 2 ( y , x ) Assumptions: x ∈ R and y ∈ R x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} x ∈ R a n d y ∈ R TeX:
\arg\!\left(x + y i\right) = \operatorname{atan2}\!\left(y, x\right)
x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument ConstI i i i Imaginary unit Atan2 atan2 ( y , x ) \operatorname{atan2}\!\left(y, x\right) a t a n 2 ( y , x ) Two-argument inverse tangent RR R \mathbb{R} R Real numbers
Source code for this entry:
Entry(ID("b2a880"),
Formula(Equal(Arg(Add(x, Mul(y, ConstI))), Atan2(y, x))),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR)))) Re ( x + y i ) = x \operatorname{Re}\!\left(x + y i\right) = x R e ( x + y i ) = x Assumptions: x ∈ R and y ∈ R x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} x ∈ R a n d y ∈ R TeX:
\operatorname{Re}\!\left(x + y i\right) = x
x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} Definitions:
Fungrim symbol Notation Short description Re Re ( z ) \operatorname{Re}\!\left(z\right) R e ( z ) Real part ConstI i i i Imaginary unit RR R \mathbb{R} R Real numbers
Source code for this entry:
Entry(ID("8e6867"),
Formula(Equal(Re(Add(x, Mul(y, ConstI))), x)),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR)))) Im ( x + y i ) = y \operatorname{Im}\!\left(x + y i\right) = y I m ( x + y i ) = y Assumptions: x ∈ R and y ∈ R x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} x ∈ R a n d y ∈ R TeX:
\operatorname{Im}\!\left(x + y i\right) = y
x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} Definitions:
Fungrim symbol Notation Short description Im Im ( z ) \operatorname{Im}\!\left(z\right) I m ( z ) Imaginary part ConstI i i i Imaginary unit RR R \mathbb{R} R Real numbers
Source code for this entry:
Entry(ID("ba6d81"),
Formula(Equal(Im(Add(x, Mul(y, ConstI))), y)),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR)))) x + y i ‾ = x − y i \overline{x + y i} = x - y i x + y i = x − y i Assumptions: x ∈ R and y ∈ R x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} x ∈ R a n d y ∈ R TeX:
\overline{x + y i} = x - y i
x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} Definitions:
Fungrim symbol Notation Short description Conjugate z ‾ \overline{z} z Complex conjugate ConstI i i i Imaginary unit RR R \mathbb{R} R Real numbers
Source code for this entry:
Entry(ID("acda23"),
Formula(Equal(Conjugate(Add(x, Mul(y, ConstI))), Sub(x, Mul(y, ConstI)))),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR)))) arg ( 1 ) = 0 \arg\!\left(1\right) = 0 arg ( 1 ) = 0 TeX:
\arg\!\left(1\right) = 0 Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument
Source code for this entry:
Entry(ID("c423d2"),
Formula(Equal(Arg(1), 0))) arg ( i ) = π 2 \arg\!\left(i\right) = \frac{\pi}{2} arg ( i ) = 2 π TeX:
\arg\!\left(i\right) = \frac{\pi}{2} Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument ConstI i i i Imaginary unit ConstPi π \pi π The constant pi (3.14...)
Source code for this entry:
Entry(ID("735409"),
Formula(Equal(Arg(ConstI), Div(ConstPi, 2)))) arg ( − i ) = − π 2 \arg\!\left(-i\right) = -\frac{\pi}{2} arg ( − i ) = − 2 π TeX:
\arg\!\left(-i\right) = -\frac{\pi}{2} Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument ConstI i i i Imaginary unit ConstPi π \pi π The constant pi (3.14...)
Source code for this entry:
Entry(ID("089f85"),
Formula(Equal(Arg(Neg(ConstI)), Neg(Div(ConstPi, 2))))) arg ( − 1 ) = π \arg\!\left(-1\right) = \pi arg ( − 1 ) = π TeX:
\arg\!\left(-1\right) = \pi Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument ConstPi π \pi π The constant pi (3.14...)
Source code for this entry:
Entry(ID("a8b41c"),
Formula(Equal(Arg(-1), ConstPi))) Re ( z ) = z + z ‾ 2 \operatorname{Re}\!\left(z\right) = \frac{z + \overline{z}}{2} R e ( z ) = 2 z + z Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\operatorname{Re}\!\left(z\right) = \frac{z + \overline{z}}{2}
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Re Re ( z ) \operatorname{Re}\!\left(z\right) R e ( z ) Real part Conjugate z ‾ \overline{z} z Complex conjugate CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("3866dc"),
Formula(Equal(Re(z), Div(Add(z, Conjugate(z)), 2))),
Variables(z),
Assumptions(Element(z, CC))) Im ( z ) = z − z ‾ 2 i \operatorname{Im}\!\left(z\right) = \frac{z - \overline{z}}{2 i} I m ( z ) = 2 i z − z Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\operatorname{Im}\!\left(z\right) = \frac{z - \overline{z}}{2 i}
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Im Im ( z ) \operatorname{Im}\!\left(z\right) I m ( z ) Imaginary part Conjugate z ‾ \overline{z} z Complex conjugate ConstI i i i Imaginary unit CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("f1a29b"),
Formula(Equal(Im(z), Div(Sub(z, Conjugate(z)), Mul(2, ConstI)))),
Variables(z),
Assumptions(Element(z, CC))) sgn ( z ) = exp ( i arg ( z ) ) \operatorname{sgn}\!\left(z\right) = \exp\!\left(i \arg\!\left(z\right)\right) s g n ( z ) = exp ( i arg ( z ) ) Assumptions: z ∈ C ∖ { 0 } z \in \mathbb{C} \setminus \left\{0\right\} z ∈ C ∖ { 0 } TeX:
\operatorname{sgn}\!\left(z\right) = \exp\!\left(i \arg\!\left(z\right)\right)
z \in \mathbb{C} \setminus \left\{0\right\} Definitions:
Fungrim symbol Notation Short description Sign sgn ( z ) \operatorname{sgn}\!\left(z\right) s g n ( z ) Sign function Exp e z {e}^{z} e z Exponential function ConstI i i i Imaginary unit Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("54340e"),
Formula(Equal(Sign(z), Exp(Mul(ConstI, Arg(z))))),
Variables(z),
Assumptions(Element(z, SetMinus(CC, Set(0))))) arg ( z ) = − i log ( sgn ( z ) ) \arg\!\left(z\right) = -i \log\!\left(\operatorname{sgn}\!\left(z\right)\right) arg ( z ) = − i log ( s g n ( z ) ) Assumptions: z ∈ C ∖ { 0 } z \in \mathbb{C} \setminus \left\{0\right\} z ∈ C ∖ { 0 } TeX:
\arg\!\left(z\right) = -i \log\!\left(\operatorname{sgn}\!\left(z\right)\right)
z \in \mathbb{C} \setminus \left\{0\right\} Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument ConstI i i i Imaginary unit Log log ( z ) \log\!\left(z\right) log ( z ) Natural logarithm Sign sgn ( z ) \operatorname{sgn}\!\left(z\right) s g n ( z ) Sign function CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("60772e"),
Formula(Equal(Arg(z), Neg(Mul(ConstI, Log(Sign(z)))))),
Variables(z),
Assumptions(Element(z, SetMinus(CC, Set(0))))) z z ‾ = ∣ z ∣ 2 z \overline{z} = {\left|z\right|}^{2} z z = ∣ z ∣ 2 Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
z \overline{z} = {\left|z\right|}^{2}
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Conjugate z ‾ \overline{z} z Complex conjugate Pow a b {a}^{b} a b Power Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("bcd22f"),
Formula(Equal(Mul(z, Conjugate(z)), Pow(Abs(z), 2))),
Variables(z),
Assumptions(Element(z, CC))) arg ( c z ) = arg ( z ) \arg\!\left(c z\right) = \arg\!\left(z\right) arg ( c z ) = arg ( z ) Assumptions: z ∈ C ∖ { 0 } and c ∈ ( 0 , ∞ ) z \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, c \in \left(0, \infty\right) z ∈ C ∖ { 0 } a n d c ∈ ( 0 , ∞ ) TeX:
\arg\!\left(c z\right) = \arg\!\left(z\right)
z \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, c \in \left(0, \infty\right) Definitions:
Fungrim symbol Notation Short description Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument CC C \mathbb{C} C Complex numbers OpenInterval ( a , b ) \left(a, b\right) ( a , b ) Open interval Infinity ∞ \infty ∞ Positive infinity
Source code for this entry:
Entry(ID("8cac46"),
Formula(Equal(Arg(Mul(c, z)), Arg(z))),
Variables(z, c),
Assumptions(And(Element(z, SetMinus(CC, Set(0))), Element(c, OpenInterval(0, Infinity))))) ∣ a b ∣ = ∣ a ∣ ∣ b ∣ \left|a b\right| = \left|a\right| \left|b\right| ∣ a b ∣ = ∣ a ∣ ∣ b ∣ Assumptions: a ∈ C and b ∈ C a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C} a ∈ C a n d b ∈ C TeX:
\left|a b\right| = \left|a\right| \left|b\right|
a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("98efc1"),
Formula(Equal(Abs(Mul(a, b)), Mul(Abs(a), Abs(b)))),
Variables(a, b),
Assumptions(And(Element(a, CC), Element(b, CC)))) ∣ a + b ∣ ≤ ∣ a ∣ + ∣ b ∣ \left|a + b\right| \le \left|a\right| + \left|b\right| ∣ a + b ∣ ≤ ∣ a ∣ + ∣ b ∣ This relation is known as the triangle inequality.
Assumptions: a ∈ C and b ∈ C a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C} a ∈ C a n d b ∈ C TeX:
\left|a + b\right| \le \left|a\right| + \left|b\right|
a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("a6e081"),
Formula(LessEqual(Abs(Add(a, b)), Add(Abs(a), Abs(b)))),
Description("This relation is known as the triangle inequality."),
Variables(a, b),
Assumptions(And(Element(a, CC), Element(b, CC)))) ∣ ∣ a ∣ − ∣ b ∣ ∣ ≤ ∣ a − b ∣ \left|\left|a\right| - \left|b\right|\right| \le \left|a - b\right| ∣ ∣ a ∣ − ∣ b ∣ ∣ ≤ ∣ a − b ∣ This relation is known as the reverse triangle inequality.
Assumptions: a ∈ C and b ∈ C a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C} a ∈ C a n d b ∈ C TeX:
\left|\left|a\right| - \left|b\right|\right| \le \left|a - b\right|
a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("48fe10"),
Formula(LessEqual(Abs(Sub(Abs(a), Abs(b))), Abs(Sub(a, b)))),
Description("This relation is known as the reverse triangle inequality."),
Variables(a, b),
Assumptions(And(Element(a, CC), Element(b, CC)))) ∣ z ‾ ∣ = ∣ z ∣ \left|\overline{z}\right| = \left|z\right| ∣ z ∣ = ∣ z ∣ Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\left|\overline{z}\right| = \left|z\right|
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value Conjugate z ‾ \overline{z} z Complex conjugate CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("6a894d"),
Formula(Equal(Abs(Conjugate(z)), Abs(z))),
Variables(z),
Assumptions(Element(z, CC))) ∣ Re ( z ) ∣ ≤ ∣ z ∣ \left|\operatorname{Re}\!\left(z\right)\right| \le \left|z\right| ∣ R e ( z ) ∣ ≤ ∣ z ∣ Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\left|\operatorname{Re}\!\left(z\right)\right| \le \left|z\right|
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value Re Re ( z ) \operatorname{Re}\!\left(z\right) R e ( z ) Real part CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("ebf8cc"),
Formula(LessEqual(Abs(Re(z)), Abs(z))),
Variables(z),
Assumptions(Element(z, CC))) ∣ Im ( z ) ∣ ≤ ∣ z ∣ \left|\operatorname{Im}\!\left(z\right)\right| \le \left|z\right| ∣ I m ( z ) ∣ ≤ ∣ z ∣ Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\left|\operatorname{Im}\!\left(z\right)\right| \le \left|z\right|
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value Im Im ( z ) \operatorname{Im}\!\left(z\right) I m ( z ) Imaginary part CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("fc427b"),
Formula(LessEqual(Abs(Im(z)), Abs(z))),
Variables(z),
Assumptions(Element(z, CC))) ∣ z ∣ ≤ ∣ Re ( z ) ∣ + ∣ Im ( z ) ∣ \left|z\right| \le \left|\operatorname{Re}\!\left(z\right)\right| + \left|\operatorname{Im}\!\left(z\right)\right| ∣ z ∣ ≤ ∣ R e ( z ) ∣ + ∣ I m ( z ) ∣ Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\left|z\right| \le \left|\operatorname{Re}\!\left(z\right)\right| + \left|\operatorname{Im}\!\left(z\right)\right|
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value Re Re ( z ) \operatorname{Re}\!\left(z\right) R e ( z ) Real part Im Im ( z ) \operatorname{Im}\!\left(z\right) I m ( z ) Imaginary part CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("12664e"),
Formula(LessEqual(Abs(z), Add(Abs(Re(z)), Abs(Im(z))))),
Variables(z),
Assumptions(Element(z, CC))) ∣ sgn ( z ) ∣ ≤ 1 \left|\operatorname{sgn}\!\left(z\right)\right| \le 1 ∣ s g n ( z ) ∣ ≤ 1 Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\left|\operatorname{sgn}\!\left(z\right)\right| \le 1
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value Sign sgn ( z ) \operatorname{sgn}\!\left(z\right) s g n ( z ) Sign function CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("432926"),
Formula(LessEqual(Abs(Sign(z)), 1)),
Variables(z),
Assumptions(Element(z, CC))) ∣ arg ( z ) ∣ ≤ π \left|\arg\!\left(z\right)\right| \le \pi ∣ arg ( z ) ∣ ≤ π Assumptions: z ∈ C z \in \mathbb{C} z ∈ C TeX:
\left|\arg\!\left(z\right)\right| \le \pi
z \in \mathbb{C} Definitions:
Fungrim symbol Notation Short description Abs ∣ z ∣ \left|z\right| ∣ z ∣ Absolute value Arg arg ( z ) \arg\!\left(z\right) arg ( z ) Complex argument ConstPi π \pi π The constant pi (3.14...) CC C \mathbb{C} C Complex numbers
Source code for this entry:
Entry(ID("08268d"),
Formula(LessEqual(Abs(Arg(z)), ConstPi)),
Variables(z),
Assumptions(Element(z, CC)))