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 an 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.