comp_ofComplex_of_im_pos

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.comp_ofComplex_of_im_pos

English

If hz > 0, then (↑ₕf) z = f ⟨z, hz⟩ for z ∈ ℂ with positive imaginary part.

Русский

Если hz > 0, то (↑ₕf) z = f ⟨z, hz⟩ для z ∈ ℂ с положительной мнимой частью.

LaTeX

$$For z ∈ ℂ with hz = 0 < Im(z), (↑ₕf) z = f ⟨z, hz⟩.$$

Lean4

theorem comp_ofComplex_of_im_pos (f : ℍ → ℂ) (z : ℂ) (hz : 0 < z.im) : (↑ₕf) z = f ⟨z, hz⟩ :=
  congrArg _ <| ofComplex_apply ⟨z, hz⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru