mathlib documentation

topology.instances.complex

@[instance]

Equations
theorem complex.dist_eq (x y : ) :
dist x y = complex.abs (x - y)

theorem complex.uniform_continuous_inv (s : set ) {r : } :
0 < r(∀ (x : ), x sr complex.abs x)uniform_continuous (λ (p : s), (p.val)⁻¹)

theorem complex.tendsto_inv {r : } :
r 0filter.tendsto (λ (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 : α → } :
(∀ (a : α), f a 0)continuous fcontinuous (λ (a : α), (f a)⁻¹)

theorem complex.uniform_continuous_mul (s : set ( × )) {r₁ r₂ : } :
(∀ (x : × ), x scomplex.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)

is homeomorphic to the real plane with max norm.

Equations