mathlib documentation

topology.instances.complex

@[instance]

def complex.metric_space :

metric_space ℂ

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}

theorem complex.dist_eq (x y : ℂ) :

dist x y = complex.abs (x - y)

theorem complex.uniform_continuous_add :

uniform_continuous (λ (p : ℂ × ℂ), p.fst + p.snd)

theorem complex.uniform_continuous_neg :

uniform_continuous has_neg.neg

@[instance]

def complex.uniform_add_group :

uniform_add_group ℂ

@[instance]

def complex.topological_add_group :

topological_add_group ℂ

theorem complex.uniform_continuous_inv (s : set ℂ) {r : ℝ} (r0 : 0 < r) (H : ∀ (x : ℂ), x ∈ s → r ≤ complex.abs x) :

uniform_continuous (λ (p : ↥s), (p.val)⁻¹)

theorem complex.uniform_continuous_abs :

uniform_continuous complex.abs

theorem complex.continuous_abs :

continuous complex.abs

theorem complex.tendsto_inv {r : ℂ} (r0 : r ≠ 0) :

(λ (q : ℂ), q⁻¹)→_{r}r⁻¹

theorem complex.continuous_inv :

continuous (λ (a : {r // r ≠ 0}), (a.val)⁻¹)

theorem complex.continuous.inv {α : Type u_1} [topological_space α] {f : α → ℂ} (h : ∀ (a : α), f a ≠ 0) (hf : continuous f) :

continuous (λ (a : α), (f a)⁻¹)

theorem complex.uniform_continuous_mul_const {x : ℂ} :

uniform_continuous (has_mul.mul x)

theorem complex.uniform_continuous_mul (s : set (ℂ × ℂ)) {r₁ r₂ : ℝ} (H : ∀ (x : ℂ × ℂ), x ∈ s → complex.abs x.fst < r₁ ∧ complex.abs x.snd < r₂) :

uniform_continuous (λ (p : ↥s), (p.val.fst) * p.val.snd)

theorem complex.continuous_mul :

continuous (λ (p : ℂ × ℂ), (p.fst) * p.snd)

theorem complex.uniform_continuous_re :

uniform_continuous complex.re

theorem complex.continuous_re :

continuous complex.re

theorem complex.uniform_continuous_im :

uniform_continuous complex.im

theorem complex.continuous_im :

continuous complex.im

theorem complex.uniform_continuous_of_real :

uniform_continuous ⇑complex.of_real

theorem complex.continuous_of_real :

continuous ⇑complex.of_real

@[instance]

def complex.topological_ring :

topological_ring ℂ

@[instance]

def complex.topological_semiring :

topological_semiring ℂ

def complex.real_prod_homeo :

ℂ ≃ₜ ℝ × ℝ

ℂ 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}

@[instance]

def complex.proper_space :

proper_space ℂ