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.isHomeomorphicTrivialFiberBundle_re: Complex.re turns ℂ into a trivial topological fiber bundle over ℝ;
• Complex.isOpenMap_re, Complex.quotientMap_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_setOf_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_setOf_re_le (a : ) :
interior {z : | z.re a} = {z : | z.re < a}
@[simp]
theorem Complex.interior_setOf_im_le (a : ) :
interior {z : | z.im a} = {z : | z.im < a}
@[simp]
theorem Complex.interior_setOf_le_re (a : ) :
interior {z : | a z.re} = {z : | a < z.re}
@[simp]
theorem Complex.interior_setOf_le_im (a : ) :
interior {z : | a z.im} = {z : | a < z.im}
@[simp]
theorem Complex.closure_setOf_re_lt (a : ) :
closure {z : | z.re < a} = {z : | z.re a}
@[simp]
theorem Complex.closure_setOf_im_lt (a : ) :
closure {z : | z.im < a} = {z : | z.im a}
@[simp]
theorem Complex.closure_setOf_lt_re (a : ) :
closure {z : | a < z.re} = {z : | a z.re}
@[simp]
theorem Complex.closure_setOf_lt_im (a : ) :
closure {z : | a < z.im} = {z : | a z.im}
@[simp]
theorem Complex.frontier_setOf_re_le (a : ) :
frontier {z : | z.re a} = {z : | z.re = a}
@[simp]
theorem Complex.frontier_setOf_im_le (a : ) :
frontier {z : | z.im a} = {z : | z.im = a}
@[simp]
theorem Complex.frontier_setOf_le_re (a : ) :
frontier {z : | a z.re} = {z : | z.re = a}
@[simp]
theorem Complex.frontier_setOf_le_im (a : ) :
frontier {z : | a z.im} = {z : | z.im = a}
@[simp]
theorem Complex.frontier_setOf_re_lt (a : ) :
frontier {z : | z.re < a} = {z : | z.re = a}
@[simp]
theorem Complex.frontier_setOf_im_lt (a : ) :
frontier {z : | z.im < a} = {z : | z.im = a}
@[simp]
theorem Complex.frontier_setOf_lt_re (a : ) :
frontier {z : | a < z.re} = {z : | z.re = a}
@[simp]
theorem Complex.frontier_setOf_lt_im (a : ) :
frontier {z : | a < z.im} = {z : | z.im = a}
theorem Complex.closure_reProdIm (s : ) (t : ) :
theorem Complex.interior_reProdIm (s : ) (t : ) :
theorem Complex.frontier_reProdIm (s : ) (t : ) :
theorem Complex.frontier_setOf_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_setOf_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 IsOpen.reProdIm {s : } {t : } (hs : ) (ht : ) :
theorem IsClosed.reProdIm {s : } {t : } (hs : ) (ht : ) :
theorem Bornology.IsBounded.reProdIm {s : } {t : } (hs : ) (ht : ) :