Theorems · Theorem · real analysis
Complex.continuousAt_cpow_of_re_pos
∀ {p : ℂ × ℂ}, 0 ≤ p.1.re ∨ p.1.im ≠ 0 → 0 < p.2.re → ContinuousAt (fun x => x.1 ^ x.2) pSee also continuousAt_cpow for a version that assumes p.1 ≠ 0 but makes no
assumptions about p.2.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 206 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 · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Complex.restatement and proof · cited by 882
- ContinuousAtstatement · cited by 697
- Complex.imstatement and proof · cited by 591
- not_and_orproof · cited by 82
- lt_iff_le_and_neproof · cited by 47
- continuousAt_cpowproof · cited by 4
- Complex.not_le_zero_iffproof · cited by 2
- Complex.continuousAt_cpow_zero_of_re_posproof · cited by 2
- Complex.not_lt_zero_iffproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Complex.continuousAt_cpow_const_of_re_posproof · cited by 2