English
A function on the upper half-plane is MDifferentiable (in the manifold-with-corners sense) iff its composition with the standard inclusion from ℂ is differentiable on the open set {z ∈ ℂ : Im z > 0}.
Русский
Функция на верхней полуплоскости MD-дифференцируема тогда и только тогда, когда композиция с включением из ℂ дифференцируема на открытом множестве {z ∈ ℂ : Im z > 0}.
LaTeX
$$$MDifferentiable 𝓘(ℂ) 𝓘(ℂ) f \;\iff\; DifferentiableOn ℂ (f \circ ofComplex) \{ z \;|\; 0 < z.im \}$$$
Lean4
theorem mdifferentiable_iff {f : ℍ → ℂ} :
MDifferentiable 𝓘(ℂ) 𝓘(ℂ) f ↔ DifferentiableOn ℂ (f ∘ ofComplex) {z | 0 < z.im} :=
⟨fun h z hz ↦ (mdifferentiableAt_iff.mp (h ⟨z, hz⟩)).differentiableWithinAt, fun h ⟨z, hz⟩ ↦
mdifferentiableAt_iff.mpr <| (h z hz).differentiableAt <| isOpen_upperHalfPlaneSet.mem_nhds hz⟩
