Theorems · Theorem · several complex variables
UpperHalfPlane.contMDiffAt_ofComplex
∀ {n : WithTop ℕ∞} {z : ℂ},
0 < z.im → ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n (↑UpperHalfPlane.ofComplex) z- Cited by
- 2 results in Mathlib
- Foundations
- Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites35
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Filterproof · cited by 8,121
- Complexstatement and proof · cited by 5,565
- nhdsproof · cited by 5,554
- ENatstatement and proof · cited by 4,985
- Filter.Tendstoproof · cited by 3,814
- WithTopstatement and proof · cited by 3,754
- modelWithCornersSelfstatement · cited by 920
- PartialHomeomorph.toPartialEquivproof · cited by 917
- OpenPartialHomeomorph.toPartialHomeomorphproof · cited by 851
- PartialEquiv.toFunproof · cited by 821
- OpenPartialHomeomorph.toFun'statement and proof · cited by 745
Cited by2
Results whose statement or proof uses this declaration.
- UpperHalfPlane.mdifferentiableAt_ofComplexproof · cited by 1
- UpperHalfPlane.contMDiffAt_iffproof · cited by 0