English
Let f be a function defined on the upper half-plane ℍ. Extend f to the whole complex plane by precomposing with the canonical embedding of ℂ into the upper half-plane. Then this extension is constant on the closed lower half-plane { z ∈ ℂ : Im(z) ≤ 0 }, i.e., for any z, z' with Im(z) ≤ 0 and Im(z') ≤ 0 we have F(z) = F(z').
Русский
Пусть f задана на верхней полуплоскости ℍ. Расширим f на всю комплексную плоскость посредством канонического вложения ℂ в верхнюю полуплоскость. Тогда полученное продолжение постоянное на замкнутой нижней полуплоскости { z ∈ ℂ : Im(z) ≤ 0 }, то есть для любых z, z' с Im(z) ≤ 0 и Im(z') ≤ 0 выполняется F(z) = F(z').
LaTeX
$$$\text{Пусть }F: \mathbb{C} \to \mathbb{C} \text{ обозначает продолжение }f\text{ на всю плоскость; тогда } \forall z,z' \in \mathbb{C},\ \Im(z) \le 0,\ \Im(z') \le 0:\ F(z) = F(z').$$$
Lean4
theorem comp_ofComplex_of_im_le_zero (f : ℍ → ℂ) (z z' : ℂ) (hz : z.im ≤ 0) (hz' : z'.im ≤ 0) : (↑ₕf) z = (↑ₕf) z' := by
simp [ofComplex_apply_of_im_nonpos, hz, hz']
