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

source
theorem complex.is_homeomorphic_trivial_fiber_bundle_re  :
is_homeomorphic_trivial_fiber_bundle ℝ complex.re

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

source
theorem complex.is_homeomorphic_trivial_fiber_bundle_im  :
is_homeomorphic_trivial_fiber_bundle ℝ complex.im

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

source
theorem complex.is_open_map_re  :
is_open_map complex.re
source
theorem complex.is_open_map_im  :
is_open_map complex.im
source
theorem complex.quotient_map_re  :
quotient_map complex.re
source
theorem complex.quotient_map_im  :
quotient_map complex.im
source
theorem complex.interior_preimage_re (s : set ℝ) :
interior (complex.re ⁻¹' s) = complex.re ⁻¹' interior s
source
theorem complex.interior_preimage_im (s : set ℝ) :
interior (complex.im ⁻¹' s) = complex.im ⁻¹' interior s
source
theorem complex.closure_preimage_re (s : set ℝ) :
closure (complex.re ⁻¹' s) = complex.re ⁻¹' closure s
source
theorem complex.closure_preimage_im (s : set ℝ) :
closure (complex.im ⁻¹' s) = complex.im ⁻¹' closure s
source
theorem complex.frontier_preimage_re (s : set ℝ) :
frontier (complex.re ⁻¹' s) = complex.re ⁻¹' frontier s
source
theorem complex.frontier_preimage_im (s : set ℝ) :
frontier (complex.im ⁻¹' s) = complex.im ⁻¹' frontier s
source
@[simp]
theorem complex.interior_set_of_re_le (a : ℝ) :
interior {z : ℂ | z.re ≤ a} = {z : ℂ | z.re < a}
source
@[simp]
theorem complex.interior_set_of_im_le (a : ℝ) :
interior {z : ℂ | z.im ≤ a} = {z : ℂ | z.im < a}
source
@[simp]
theorem complex.interior_set_of_le_re (a : ℝ) :
interior {z : ℂ | a ≤ z.re} = {z : ℂ | a < z.re}
source
@[simp]
theorem complex.interior_set_of_le_im (a : ℝ) :
interior {z : ℂ | a ≤ z.im} = {z : ℂ | a < z.im}
source
@[simp]
theorem complex.closure_set_of_re_lt (a : ℝ) :
closure {z : ℂ | z.re < a} = {z : ℂ | z.re ≤ a}
source
@[simp]
theorem complex.closure_set_of_im_lt (a : ℝ) :
closure {z : ℂ | z.im < a} = {z : ℂ | z.im ≤ a}
source
@[simp]
theorem complex.closure_set_of_lt_re (a : ℝ) :
closure {z : ℂ | a < z.re} = {z : ℂ | a ≤ z.re}
source
@[simp]
theorem complex.closure_set_of_lt_im (a : ℝ) :
closure {z : ℂ | a < z.im} = {z : ℂ | a ≤ z.im}
source
@[simp]
theorem complex.frontier_set_of_re_le (a : ℝ) :
frontier {z : ℂ | z.re ≤ a} = {z : ℂ | z.re = a}
source
@[simp]
theorem complex.frontier_set_of_im_le (a : ℝ) :
frontier {z : ℂ | z.im ≤ a} = {z : ℂ | z.im = a}
source
@[simp]
theorem complex.frontier_set_of_le_re (a : ℝ) :
frontier {z : ℂ | a ≤ z.re} = {z : ℂ | z.re = a}
source
@[simp]
theorem complex.frontier_set_of_le_im (a : ℝ) :
frontier {z : ℂ | a ≤ z.im} = {z : ℂ | z.im = a}
source
@[simp]
theorem complex.frontier_set_of_re_lt (a : ℝ) :
frontier {z : ℂ | z.re < a} = {z : ℂ | z.re = a}
source
@[simp]
theorem complex.frontier_set_of_im_lt (a : ℝ) :
frontier {z : ℂ | z.im < a} = {z : ℂ | z.im = a}
source
@[simp]
theorem complex.frontier_set_of_lt_re (a : ℝ) :
frontier {z : ℂ | a < z.re} = {z : ℂ | z.re = a}
source
@[simp]
theorem complex.frontier_set_of_lt_im (a : ℝ) :
frontier {z : ℂ | a < z.im} = {z : ℂ | z.im = a}
source
theorem complex.closure_re_prod_im (s t : set ℝ) :
closure (s ×ℂ t) = closure s ×ℂ closure t
source
theorem complex.interior_re_prod_im (s t : set ℝ) :
interior (s ×ℂ t) = interior s ×ℂ interior t
source
theorem complex.frontier_re_prod_im (s t : set ℝ) :
frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t
source
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}
source
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}
source
theorem is_open.re_prod_im {s t : set ℝ} (hs : is_open s) (ht : is_open t) :
is_open (s ×ℂ t)
source
theorem is_closed.re_prod_im {s t : set ℝ} (hs : is_closed s) (ht : is_closed t) :
is_closed (s ×ℂ t)
source
theorem metric.bounded.re_prod_im {s t : set ℝ} (hs : metric.bounded s) (ht : metric.bounded t) :
metric.bounded (s ×ℂ t)