coe_mk_subtype

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

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

English

For any z ∈ ℂ with Im(z) > 0, the coercion of the subtype element ⟨z, h⟩ to ℂ is z.

Русский

Для любого z ∈ ℂ с Im(z) > 0 коэрцирование элемента подтипа ⟨z, h⟩ к ℂ даёт z.

LaTeX

$$$\\UpperHalfPlane.coe\\langle z, h \\rangle = z$$$

Lean4

@[simp]
theorem coe_mk_subtype {z : ℂ} (hz : 0 < z.im) : UpperHalfPlane.coe ⟨z, hz⟩ = z := by rfl

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

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

Разделы

Аффилиация

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