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 forinterior (Complex.re ⁻¹' s)
etc;Complex.interior_setOf_re_le
etc: particular cases of the above formulas in the cases whens
is one of the infinite intervalsSet.Ioi a
,Set.Ici a
,Set.Iio a
, andSet.Iic a
, formulated asinterior {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 ℝ
.
theorem
Complex.interior_preimage_re
(s : Set ℝ)
:
interior (Complex.re ⁻¹' s) = Complex.re ⁻¹' interior s
theorem
Complex.interior_preimage_im
(s : Set ℝ)
:
interior (Complex.im ⁻¹' s) = Complex.im ⁻¹' interior s
theorem
Complex.closure_preimage_re
(s : Set ℝ)
:
closure (Complex.re ⁻¹' s) = Complex.re ⁻¹' closure s
theorem
Complex.closure_preimage_im
(s : Set ℝ)
:
closure (Complex.im ⁻¹' s) = Complex.im ⁻¹' closure s
theorem
Complex.frontier_preimage_re
(s : Set ℝ)
:
frontier (Complex.re ⁻¹' s) = Complex.re ⁻¹' frontier s
theorem
Complex.frontier_preimage_im
(s : Set ℝ)
:
frontier (Complex.im ⁻¹' s) = Complex.im ⁻¹' frontier s
theorem
Bornology.IsBounded.reProdIm
{s : Set ℝ}
{t : Set ℝ}
(hs : Bornology.IsBounded s)
(ht : Bornology.IsBounded t)
:
Bornology.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