Complex plane

77ef0c

\mathbb{C} = \left\{ x + y i : x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \right\}

TeX:

\mathbb{C} = \left\{ x + y i : x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \right\}

Definitions:

Fungrim symbol	Notation	Short description
`CC`	$\mathbb{C}$	Complex numbers
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`ConstI`	$i$	Imaginary unit
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("77ef0c"),
    Formula(Equal(CC, SetBuilder(Add(x, Mul(y, ConstI)), Tuple(x, y), And(Element(x, RR), Element(y, RR))))))

a65a14

Symbol: HH —

\mathbb{H}

— Upper complex half-plane

Represents the set of complex numbers with strictly positive imaginary part.

Definitions:

Fungrim symbol	Notation	Short description
`HH`	$\mathbb{H}$	Upper complex half-plane

Source code for this entry:

Entry(ID("a65a14"),
    SymbolDefinition(HH, HH, "Upper complex half-plane"),
    Description("Represents the set of complex numbers with strictly positive imaginary part."))

d7962e

\mathbb{H} = \left\{ \tau : \tau \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \operatorname{Im}\!\left(\tau\right) \gt 0 \right\}

TeX:

\mathbb{H} = \left\{ \tau : \tau \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \operatorname{Im}\!\left(\tau\right) \gt 0 \right\}

Definitions:

Fungrim symbol	Notation	Short description
`HH`	$\mathbb{H}$	Upper complex half-plane
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`CC`	$\mathbb{C}$	Complex numbers
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part

Source code for this entry:

Entry(ID("d7962e"),
    Formula(Equal(HH, SetBuilder(tau, tau, And(Element(tau, CC), Greater(Im(tau), 0))))))

fc0d55

\mathbb{T} = \left\{ z : z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z\right| = 1 \right\}

TeX:

\mathbb{T} = \left\{ z : z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z\right| = 1 \right\}

Definitions:

Fungrim symbol	Notation	Short description
`UnitCircle`	$\mathbb{T}$	Unit circle
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value

Source code for this entry:

Entry(ID("fc0d55"),
    Formula(Equal(UnitCircle, SetBuilder(z, z, And(Element(z, CC), Equal(Abs(z), 1))))))

912ff9

\mathbb{T} = \left\{ {e}^{i \theta} : \theta \in \left[0, 2 \pi\right) \right\}

TeX:

\mathbb{T} = \left\{ {e}^{i \theta} : \theta \in \left[0, 2 \pi\right) \right\}

Definitions:

Fungrim symbol	Notation	Short description
`UnitCircle`	$\mathbb{T}$	Unit circle
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`Exp`	${e}^{z}$	Exponential function
`ConstI`	$i$	Imaginary unit
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`ConstPi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("912ff9"),
    Formula(Equal(UnitCircle, SetBuilder(Exp(Mul(ConstI, theta)), theta, Element(theta, ClosedOpenInterval(0, Mul(2, ConstPi)))))))

c98bad

\operatorname{OpenDisk}\!\left(z, r\right) = \left\{ t : t \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z - t\right| \lt r \right\}

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, r \in \mathbb{R} \,\mathbin{\operatorname{and}}\, r \gt 0

TeX:

\operatorname{OpenDisk}\!\left(z, r\right) = \left\{ t : t \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z - t\right| \lt r \right\}

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, r \in \mathbb{R} \,\mathbin{\operatorname{and}}\, r \gt 0

Definitions:

Fungrim symbol	Notation	Short description
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("c98bad"),
    Formula(Equal(OpenDisk(z, r), SetBuilder(t, t, And(Element(t, CC), Less(Abs(Sub(z, t)), r))))),
    Variables(z, r),
    Assumptions(And(Element(z, CC), Element(r, RR), Greater(r, 0))))

d1cf0c

\operatorname{ClosedDisk}\!\left(z, r\right) = \left\{ t : t \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z - t\right| \le r \right\}

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, r \in \mathbb{R} \,\mathbin{\operatorname{and}}\, r \ge 0

TeX:

\operatorname{ClosedDisk}\!\left(z, r\right) = \left\{ t : t \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \left|z - t\right| \le r \right\}

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, r \in \mathbb{R} \,\mathbin{\operatorname{and}}\, r \ge 0

Definitions:

Fungrim symbol	Notation	Short description
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("d1cf0c"),
    Formula(Equal(ClosedDisk(z, r), SetBuilder(t, t, And(Element(t, CC), LessEqual(Abs(Sub(z, t)), r))))),
    Variables(z, r),
    Assumptions(And(Element(z, CC), Element(r, RR), GreaterEqual(r, 0))))

40baa9

\mathcal{E}_{\rho} = \left\{ \frac{\rho {e}^{i \theta} + {\rho}^{-1} {e}^{-i \theta}}{2} : \theta \in \left[0, 2 \pi\right) \right\}

Assumptions:

\rho \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \rho \gt 1

TeX:

\mathcal{E}_{\rho} = \left\{ \frac{\rho {e}^{i \theta} + {\rho}^{-1} {e}^{-i \theta}}{2} : \theta \in \left[0, 2 \pi\right) \right\}

\rho \in \mathbb{R} \,\mathbin{\operatorname{and}}\, \rho \gt 1

Definitions:

Fungrim symbol	Notation	Short description
`BernsteinEllipse`	$\mathcal{E}_{\rho}$	Bernstein ellipse with foci -1,+1 and semi-axis sum rho
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`Exp`	${e}^{z}$	Exponential function
`ConstI`	$i$	Imaginary unit
`Pow`	${a}^{b}$	Power
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`ConstPi`	$\pi$	The constant pi (3.14...)
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("40baa9"),
    Formula(Equal(BernsteinEllipse(rho), SetBuilder(Div(Add(Mul(rho, Exp(Mul(ConstI, theta))), Mul(Pow(rho, -1), Exp(Neg(Mul(ConstI, theta))))), 2), theta, Element(theta, ClosedOpenInterval(0, Mul(2, ConstPi)))))),
    Variables(rho),
    Assumptions(And(Element(rho, RR), Greater(rho, 1))))

Main regions

Disks

Bernstein ellipses