Theorems · Theorem · complex analysis
Complex.continuousAt_sqrt
∀ {z : ℂ}, 0 ≤ z.re ∨ z.im ≠ 0 → ContinuousAt Complex.sqrt zComplex.sqrt is continuous at z provided 0 ≤ z.re or z.im ≠ 0. This is weaker than
requiring z ∈ slitPlane, as it additionally includes the imaginary axis and 0.
- Defined in
- Mathlib.Analysis.Complex.SqrtDeriv
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- Complex.restatement and proof · cited by 882
- ContinuousAtstatement · cited by 697
- one_divproof · cited by 624
- Complex.imstatement and proof · cited by 591
- Complex.sqrtstatement · cited by 32
- Complex.div_ofNat_reproof · cited by 7
- Complex.continuousAt_cpow_const_of_re_posproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- Complex.continuousOn_sqrtproof · cited by 0