English
The product of a real set s and an imaginary set t on the complex plane is the set of complex numbers whose real part lies in s and imaginary part lies in t.
Русский
Произведение множеств по вещественной и мнимой оси на комплексной плоскости состоит из чисел z, у которых Re(z) ∈ s и Im(z) ∈ t.
LaTeX
$$$\\\\mathrm{reProdIm}(s,t) = \\{ z \\\\in \\\\mathbb{C} \\\\:| \\\\operatorname{Re}(z) \\\\in s \\\\land \\\\operatorname{Im}(z) \\\\in t \\}.$$$
Lean4
/-- The product of a set on the real axis and a set on the imaginary axis of the complex plane,
denoted by `s ×ℂ t`. -/
def reProdIm (s t : Set ℝ) : Set ℂ :=
re ⁻¹' s ∩ im ⁻¹' t
