@[instance]
Equations
- complex.metric_space = {to_has_dist := {dist := λ (x y : ℂ), complex.abs (x - y)}, dist_self := complex.metric_space._proof_1, eq_of_dist_eq_zero := complex.metric_space._proof_2, dist_comm := complex.metric_space._proof_3, dist_triangle := complex.metric_space._proof_4, edist := λ (x y : ℂ), ennreal.of_real ((λ (x y : ℂ), complex.abs (x - y)) x y), edist_dist := complex.metric_space._proof_5, to_uniform_space := uniform_space_of_dist (λ (x y : ℂ), complex.abs (x - y)) complex.metric_space._proof_6 complex.metric_space._proof_7 complex.metric_space._proof_8, uniformity_dist := complex.metric_space._proof_9}
@[instance]
Equations
@[instance]
theorem
complex.uniform_continuous_inv
(s : set ℂ)
{r : ℝ} :
0 < r → (∀ (x : ℂ), x ∈ s → r ≤ complex.abs x) → uniform_continuous (λ (p : ↥s), (p.val)⁻¹)
theorem
complex.continuous.inv
{α : Type u_1}
[topological_space α]
{f : α → ℂ} :
(∀ (a : α), f a ≠ 0) → continuous f → continuous (λ (a : α), (f a)⁻¹)
@[instance]
Equations
@[instance]
Equations
ℂ is homeomorphic to the real plane with max norm.
Equations
- complex.real_prod_homeo = {to_equiv := complex.equiv_real_prod, continuous_to_fun := complex.real_prod_homeo._proof_1, continuous_inv_fun := complex.real_prod_homeo._proof_2}