mathlib3 documentation

analysis.complex.re_im_topology

Closure, interior, and frontier of preimages under re and im #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this fact we use the fact that is naturally homeomorphic to ℝ × ℝ to deduce some topological properties of complex.re and complex.im.

Main statements #

Each statement about complex.re listed below has a counterpart about complex.im.

Tags #

complex, real part, imaginary part, closure, interior, frontier

complex.re turns into a trivial topological fiber bundle over .

complex.im turns into a trivial topological fiber bundle over .

@[simp]
theorem complex.interior_set_of_re_le (a : ) :
interior {z : | z.re a} = {z : | z.re < a}
@[simp]
theorem complex.interior_set_of_im_le (a : ) :
interior {z : | z.im a} = {z : | z.im < a}
@[simp]
theorem complex.interior_set_of_le_re (a : ) :
interior {z : | a z.re} = {z : | a < z.re}
@[simp]
theorem complex.interior_set_of_le_im (a : ) :
interior {z : | a z.im} = {z : | a < z.im}
@[simp]
theorem complex.closure_set_of_re_lt (a : ) :
closure {z : | z.re < a} = {z : | z.re a}
@[simp]
theorem complex.closure_set_of_im_lt (a : ) :
closure {z : | z.im < a} = {z : | z.im a}
@[simp]
theorem complex.closure_set_of_lt_re (a : ) :
closure {z : | a < z.re} = {z : | a z.re}
@[simp]
theorem complex.closure_set_of_lt_im (a : ) :
closure {z : | a < z.im} = {z : | a z.im}
@[simp]
theorem complex.frontier_set_of_re_le (a : ) :
frontier {z : | z.re a} = {z : | z.re = a}
@[simp]
theorem complex.frontier_set_of_im_le (a : ) :
frontier {z : | z.im a} = {z : | z.im = a}
@[simp]
theorem complex.frontier_set_of_le_re (a : ) :
frontier {z : | a z.re} = {z : | z.re = a}
@[simp]
theorem complex.frontier_set_of_le_im (a : ) :
frontier {z : | a z.im} = {z : | z.im = a}
@[simp]
theorem complex.frontier_set_of_re_lt (a : ) :
frontier {z : | z.re < a} = {z : | z.re = a}
@[simp]
theorem complex.frontier_set_of_im_lt (a : ) :
frontier {z : | z.im < a} = {z : | z.im = a}
@[simp]
theorem complex.frontier_set_of_lt_re (a : ) :
frontier {z : | a < z.re} = {z : | z.re = a}
@[simp]
theorem complex.frontier_set_of_lt_im (a : ) :
frontier {z : | a < z.im} = {z : | z.im = a}
theorem complex.frontier_set_of_le_re_and_le_im (a b : ) :
frontier {z : | a z.re b z.im} = {z : | a z.re z.im = b z.re = a b z.im}
theorem complex.frontier_set_of_le_re_and_im_le (a b : ) :
frontier {z : | a z.re z.im b} = {z : | a z.re z.im = b z.re = a z.im b}
theorem is_open.re_prod_im {s t : set } (hs : is_open s) (ht : is_open t) :
theorem is_closed.re_prod_im {s t : set } (hs : is_closed s) (ht : is_closed t) :