ofComplex_apply_of_im_pos

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

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

English

If z ∈ ℂ has positive imaginary part, then ofComplex z = ⟨z, hz⟩ for hz = 0 < Im(z).

Русский

Если z ∈ ℂ имеет положительную мнимую часть, то ofComplex z = ⟨z, hz⟩ с hz = 0 < Im(z).

LaTeX

$$ofComplex(z) = ⟨z, hz⟩ for hz with hz = 0 < Im(z).$$

Lean4

theorem ofComplex_apply_of_im_pos {z : ℂ} (hz : 0 < z.im) : ofComplex z = ⟨z, hz⟩ := by
  simpa only [coe_mk_subtype] using ofComplex_apply ⟨z, hz⟩

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

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

Разделы

Аффилиация

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