Half-planes in ℂ are open

We state that open left, right, upper and lower half-planes in the complex numbers are open sets, where the bounding value of the real or imaginary part is given by a real or EReal x. So this includes the full plane and the empty set for x = ⊤/x = ⊥.

theorem Complex.isOpen_re_lt_EReal (x : EReal) : IsOpen {z : ℂ | ↑z.re < x}

An open left half-plane (with boundary real part given by an EReal) is an open set in the complex plane.

theorem Complex.isOpen_re_gt_EReal (x : EReal) : IsOpen {z : ℂ | x < ↑z.re}

An open right half-plane (with boundary real part given by an EReal) is an open set in the complex plane.

theorem Complex.isOpen_im_lt_EReal (x : EReal) : IsOpen {z : ℂ | ↑z.im < x}

An open lower half-plane (with boundary imaginary part given by an EReal) is an open set in the complex plane.

theorem Complex.isOpen_im_gt_EReal (x : EReal) : IsOpen {z : ℂ | x < ↑z.im}

An open upper half-plane (with boundary imaginary part given by an EReal) is an open set in the complex plane.

theorem Complex.isOpen_re_lt (x : ℝ) : IsOpen {z : ℂ | z.re < x}

An open left half-plane is an open set in the complex plane.

theorem Complex.isOpen_re_gt (x : ℝ) : IsOpen {z : ℂ | x < z.re}

An open right half-plane is an open set in the complex plane.

theorem Complex.isOpen_im_lt (x : ℝ) : IsOpen {z : ℂ | z.im < x}

An open lower half-plane is an open set in the complex plane.

theorem Complex.isOpen_im_gt (x : ℝ) : IsOpen {z : ℂ | x < z.im}

An open upper half-plane is an open set in the complex plane.