coe_im — Mathlib

English

Let z lie in the upper half-plane ℍ. Then the imaginary part of z, viewed as a complex number, equals the imaginary-part coordinate of z (the ℍ-coordinate).

Русский

Пусть z принадлежит верхней полуплоскости ℍ. Тогда мнимая часть z, считая z как число на комплексной плоскости, равна мнимой координате z.

LaTeX

$$$$ \\forall z \\in \\mathbb{H},\\ \\operatorname{Im}(z) = z.\\operatorname{im} $$$$

Lean4

@[simp]
theorem coe_im (z : ℍ) : (z : ℂ).im = z.im :=
  rfl

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