HepLean Documentation

Mathlib.Analysis.Complex.ReImTopology

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.

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 .

@[deprecated Complex.isQuotientMap_re]

Alias of Complex.isQuotientMap_re.

@[deprecated Complex.isQuotientMap_im]

Alias of Complex.isQuotientMap_im.

@[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.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 : Set } {t : Set } (hs : IsOpen s) (ht : IsOpen t) :
theorem IsClosed.reProdIm {s : Set } {t : Set } (hs : IsClosed s) (ht : IsClosed t) :
theorem TendstoUniformlyOn.re {α : Type u_1} {ι : Type u_2} {f : ια} {p : Filter ι} {g : α} {K : Set α} (hf : TendstoUniformlyOn f g p K) :
TendstoUniformlyOn (fun (n : ι) (x : α) => (f n x).re) (fun (y : α) => (g y).re) p K
theorem TendstoUniformly.re {α : Type u_1} {ι : Type u_2} {f : ια} {p : Filter ι} {g : α} (hf : TendstoUniformly f g p) :
TendstoUniformly (fun (n : ι) (x : α) => (f n x).re) (fun (y : α) => (g y).re) p
theorem TendstoUniformlyOn.im {α : Type u_1} {ι : Type u_2} {f : ια} {p : Filter ι} {g : α} {K : Set α} (hf : TendstoUniformlyOn f g p K) :
TendstoUniformlyOn (fun (n : ι) (x : α) => (f n x).im) (fun (y : α) => (g y).im) p K
theorem TendstoUniformly.im {α : Type u_1} {ι : Type u_2} {f : ια} {p : Filter ι} {g : α} (hf : TendstoUniformly f g p) :
TendstoUniformly (fun (n : ι) (x : α) => (f n x).im) (fun (y : α) => (g y).im) p