# mathlibdocumentation

analysis.complex.re_im_topology

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

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.

• complex.is_trivial_topological_fiber_bundle_re: complex.re turns ℂ into a trivial topological fiber bundle over ℝ;
• complex.is_open_map_re, complex.quotient_map_re: in particular, complex.re is an open map and is a quotient map;
• complex.interior_preimage_re, complex.closure_preimage_re, complex.frontier_preimage_re: formulas for interior (complex.re ⁻¹' s) etc;
• complex.interior_set_of_re_le etc: particular cases of the above formulas in the cases when s is one of the infinite intervals set.Ioi a, set.Ici a, set.Iio a, and set.Iic a, formulated as interior {z : ℂ | z.re ≤ a} = {z | z.re < a} etc.

## 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) :