Points of large norm in a coordinate half-plane of ℂ

Each of the four inequalities z.im < c, c < z.im, z.re < c and c < z.re cuts out an open half-plane of ℂ — two horizontal, two vertical — and each holds points of arbitrarily large norm. These are the specialisations of TauCeti.exists_apply_lt_and_lt_norm and TauCeti.exists_lt_apply_and_lt_norm to Complex.reLm and Complex.imLm.

This is what a winding-number vanishing argument needs: to transport a winding number through an unbounded connected region one must exhibit, for each radius, a point of the region beyond it.

Main results

• Complex.reLm_ne_zero, Complex.imLm_ne_zero — the two coordinate functionals of ℂ are nonzero.
• TauCeti.exists_im_lt_and_lt_norm, TauCeti.exists_lt_im_and_lt_norm, TauCeti.exists_re_lt_and_lt_norm, TauCeti.exists_lt_re_and_lt_norm — the four coordinate half-planes.

@[simp]

theorem Complex.imLm_ne_zero : imLm ≠ 0

The imaginary part is not the zero functional.

@[simp]

theorem Complex.reLm_ne_zero : reLm ≠ 0

The real part is not the zero functional.

theorem TauCeti.exists_im_lt_and_lt_norm (c R : ℝ) : ∃ (z : ℂ), z.im < c ∧ R < ‖z‖

The open lower half-plane {z | z.im < c} contains points of arbitrarily large norm.

theorem TauCeti.exists_lt_im_and_lt_norm (c R : ℝ) : ∃ (z : ℂ), c < z.im ∧ R < ‖z‖

The open upper half-plane {z | c < z.im} contains points of arbitrarily large norm.

theorem TauCeti.exists_re_lt_and_lt_norm (c R : ℝ) : ∃ (z : ℂ), z.re < c ∧ R < ‖z‖

The open left half-plane {z | z.re < c} contains points of arbitrarily large norm.

theorem TauCeti.exists_lt_re_and_lt_norm (c R : ℝ) : ∃ (z : ℂ), c < z.re ∧ R < ‖z‖

The open right half-plane {z | c < z.re} contains points of arbitrarily large norm.