mk_re — Mathlib

English

For any complex number z and any h with z.im > 0, the real part of the constructed point mk z h equals z.re.

Русский

Пусть z ∈ ℂ и h > 0 удовлетворяет z.im > 0. Тогда действительная часть mk z h равна z.re.

LaTeX

$$$$ \\forall z \\in \\mathbb{C},\\ \\forall h > 0,\\ \\operatorname{Re}(\\mathrm{mk}(z,h)) = \\operatorname{Re}(z) $$$$

Lean4

@[simp]
theorem mk_re (z : ℂ) (h : 0 < z.im) : (mk z h).re = z.re :=
  rfl

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