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.isQuotientMap_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_setOfPred_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

theorem Complex.isHomeomorphicTrivialFiberBundle_re : IsHomeomorphicTrivialFiberBundle ℝ re

Complex.re turns ℂ into a trivial topological fiber bundle over ℝ.

theorem Complex.isHomeomorphicTrivialFiberBundle_im : IsHomeomorphicTrivialFiberBundle ℝ im

Complex.im turns ℂ into a trivial topological fiber bundle over ℝ.

theorem Complex.isOpenMap_re : IsOpenMap re

theorem Complex.isOpenMap_im : IsOpenMap im

theorem Complex.isQuotientMap_re : Topology.IsQuotientMap re

theorem Complex.isQuotientMap_im : Topology.IsQuotientMap im

theorem Complex.interior_preimage_re (s : Set ℝ) : interior (re ⁻¹' s) = re ⁻¹' interior s

theorem Complex.interior_preimage_im (s : Set ℝ) : interior (im ⁻¹' s) = im ⁻¹' interior s

theorem Complex.closure_preimage_re (s : Set ℝ) : closure (re ⁻¹' s) = re ⁻¹' closure s

theorem Complex.closure_preimage_im (s : Set ℝ) : closure (im ⁻¹' s) = im ⁻¹' closure s

theorem Complex.frontier_preimage_re (s : Set ℝ) : frontier (re ⁻¹' s) = re ⁻¹' frontier s

theorem Complex.frontier_preimage_im (s : Set ℝ) : frontier (im ⁻¹' s) = im ⁻¹' frontier s

@[simp]

theorem Complex.interior_setOfPred_re_le (a : ℝ) : interior {z : ℂ | z.re ≤ a} = {z : ℂ | z.re < a}

@[deprecated Complex.interior_setOfPred_re_le (since := "2026-07-09")]

theorem Complex.interior_setOf_re_le (a : ℝ) : interior {z : ℂ | z.re ≤ a} = {z : ℂ | z.re < a}

Alias of Complex.interior_setOfPred_re_le.

@[simp]

theorem Complex.interior_setOfPred_im_le (a : ℝ) : interior {z : ℂ | z.im ≤ a} = {z : ℂ | z.im < a}

@[deprecated Complex.interior_setOfPred_im_le (since := "2026-07-09")]

theorem Complex.interior_setOf_im_le (a : ℝ) : interior {z : ℂ | z.im ≤ a} = {z : ℂ | z.im < a}

Alias of Complex.interior_setOfPred_im_le.

@[simp]

theorem Complex.interior_setOfPred_le_re (a : ℝ) : interior {z : ℂ | a ≤ z.re} = {z : ℂ | a < z.re}

@[deprecated Complex.interior_setOfPred_le_re (since := "2026-07-09")]

theorem Complex.interior_setOf_le_re (a : ℝ) : interior {z : ℂ | a ≤ z.re} = {z : ℂ | a < z.re}

Alias of Complex.interior_setOfPred_le_re.

@[simp]

theorem Complex.interior_setOfPred_le_im (a : ℝ) : interior {z : ℂ | a ≤ z.im} = {z : ℂ | a < z.im}

@[deprecated Complex.interior_setOfPred_le_im (since := "2026-07-09")]

theorem Complex.interior_setOf_le_im (a : ℝ) : interior {z : ℂ | a ≤ z.im} = {z : ℂ | a < z.im}

Alias of Complex.interior_setOfPred_le_im.

@[simp]

theorem Complex.closure_setOfPred_re_lt (a : ℝ) : closure {z : ℂ | z.re < a} = {z : ℂ | z.re ≤ a}

@[deprecated Complex.closure_setOfPred_re_lt (since := "2026-07-09")]

theorem Complex.closure_setOf_re_lt (a : ℝ) : closure {z : ℂ | z.re < a} = {z : ℂ | z.re ≤ a}

Alias of Complex.closure_setOfPred_re_lt.

@[simp]

theorem Complex.closure_setOfPred_im_lt (a : ℝ) : closure {z : ℂ | z.im < a} = {z : ℂ | z.im ≤ a}

@[deprecated Complex.closure_setOfPred_im_lt (since := "2026-07-09")]

theorem Complex.closure_setOf_im_lt (a : ℝ) : closure {z : ℂ | z.im < a} = {z : ℂ | z.im ≤ a}

Alias of Complex.closure_setOfPred_im_lt.

@[simp]

theorem Complex.closure_setOfPred_lt_re (a : ℝ) : closure {z : ℂ | a < z.re} = {z : ℂ | a ≤ z.re}

@[deprecated Complex.closure_setOfPred_lt_re (since := "2026-07-09")]

theorem Complex.closure_setOf_lt_re (a : ℝ) : closure {z : ℂ | a < z.re} = {z : ℂ | a ≤ z.re}

Alias of Complex.closure_setOfPred_lt_re.

@[simp]

theorem Complex.closure_setOfPred_lt_im (a : ℝ) : closure {z : ℂ | a < z.im} = {z : ℂ | a ≤ z.im}

@[deprecated Complex.closure_setOfPred_lt_im (since := "2026-07-09")]

theorem Complex.closure_setOf_lt_im (a : ℝ) : closure {z : ℂ | a < z.im} = {z : ℂ | a ≤ z.im}

Alias of Complex.closure_setOfPred_lt_im.

@[simp]

theorem Complex.frontier_setOfPred_re_le (a : ℝ) : frontier {z : ℂ | z.re ≤ a} = {z : ℂ | z.re = a}

@[deprecated Complex.frontier_setOfPred_re_le (since := "2026-07-09")]

theorem Complex.frontier_setOf_re_le (a : ℝ) : frontier {z : ℂ | z.re ≤ a} = {z : ℂ | z.re = a}

Alias of Complex.frontier_setOfPred_re_le.

@[simp]

theorem Complex.frontier_setOfPred_im_le (a : ℝ) : frontier {z : ℂ | z.im ≤ a} = {z : ℂ | z.im = a}

@[deprecated Complex.frontier_setOfPred_im_le (since := "2026-07-09")]

theorem Complex.frontier_setOf_im_le (a : ℝ) : frontier {z : ℂ | z.im ≤ a} = {z : ℂ | z.im = a}

Alias of Complex.frontier_setOfPred_im_le.

@[simp]

theorem Complex.frontier_setOfPred_le_re (a : ℝ) : frontier {z : ℂ | a ≤ z.re} = {z : ℂ | z.re = a}

@[deprecated Complex.frontier_setOfPred_le_re (since := "2026-07-09")]

theorem Complex.frontier_setOf_le_re (a : ℝ) : frontier {z : ℂ | a ≤ z.re} = {z : ℂ | z.re = a}

Alias of Complex.frontier_setOfPred_le_re.

@[simp]

theorem Complex.frontier_setOfPred_le_im (a : ℝ) : frontier {z : ℂ | a ≤ z.im} = {z : ℂ | z.im = a}

@[deprecated Complex.frontier_setOfPred_le_im (since := "2026-07-09")]

theorem Complex.frontier_setOf_le_im (a : ℝ) : frontier {z : ℂ | a ≤ z.im} = {z : ℂ | z.im = a}

Alias of Complex.frontier_setOfPred_le_im.

@[simp]

theorem Complex.frontier_setOfPred_re_lt (a : ℝ) : frontier {z : ℂ | z.re < a} = {z : ℂ | z.re = a}

@[deprecated Complex.frontier_setOfPred_re_lt (since := "2026-07-09")]

theorem Complex.frontier_setOf_re_lt (a : ℝ) : frontier {z : ℂ | z.re < a} = {z : ℂ | z.re = a}

Alias of Complex.frontier_setOfPred_re_lt.

@[simp]

theorem Complex.frontier_setOfPred_im_lt (a : ℝ) : frontier {z : ℂ | z.im < a} = {z : ℂ | z.im = a}

@[deprecated Complex.frontier_setOfPred_im_lt (since := "2026-07-09")]

theorem Complex.frontier_setOf_im_lt (a : ℝ) : frontier {z : ℂ | z.im < a} = {z : ℂ | z.im = a}

Alias of Complex.frontier_setOfPred_im_lt.

@[simp]

theorem Complex.frontier_setOfPred_lt_re (a : ℝ) : frontier {z : ℂ | a < z.re} = {z : ℂ | z.re = a}

@[deprecated Complex.frontier_setOfPred_lt_re (since := "2026-07-09")]

theorem Complex.frontier_setOf_lt_re (a : ℝ) : frontier {z : ℂ | a < z.re} = {z : ℂ | z.re = a}

Alias of Complex.frontier_setOfPred_lt_re.

@[simp]

theorem Complex.frontier_setOfPred_lt_im (a : ℝ) : frontier {z : ℂ | a < z.im} = {z : ℂ | z.im = a}

@[deprecated Complex.frontier_setOfPred_lt_im (since := "2026-07-09")]

theorem Complex.frontier_setOf_lt_im (a : ℝ) : frontier {z : ℂ | a < z.im} = {z : ℂ | z.im = a}

Alias of Complex.frontier_setOfPred_lt_im.

theorem Complex.closure_reProdIm (s t : Set ℝ) : closure (s ×ℂ t) = closure s ×ℂ closure t

theorem Complex.interior_reProdIm (s t : Set ℝ) : interior (s ×ℂ t) = interior s ×ℂ interior t

theorem Complex.frontier_reProdIm (s t : Set ℝ) : frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t

theorem Complex.frontier_setOfPred_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}

@[deprecated Complex.frontier_setOfPred_le_re_and_le_im (since := "2026-07-09")]

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}

Alias of Complex.frontier_setOfPred_le_re_and_le_im.

theorem Complex.frontier_setOfPred_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}

@[deprecated Complex.frontier_setOfPred_le_re_and_im_le (since := "2026-07-09")]

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}

Alias of Complex.frontier_setOfPred_le_re_and_im_le.

theorem IsOpen.reProdIm {s t : Set ℝ} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ×ℂ t)

theorem IsClosed.reProdIm {s t : Set ℝ} (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ×ℂ t)

theorem Bornology.IsBounded.reProdIm {s t : Set ℝ} (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ×ℂ 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