coe_mem_integerComplement — Mathlib

English

If z lies in the upper half-plane, then its complex value belongs to the integer complement set.

Русский

Если z лежит в верхней полуплоскости, то его комплексное значение принадлежит множеству дополнения целых.

LaTeX

$$$\\forall z \\in \\mathbb{H}, \\; z \\in \\mathbb{C}_{\\mathbb{Z}}.$$$

Lean4

theorem coe_mem_integerComplement (z : ℍ) : ↑z ∈ ℂ_ℤ :=
  not_exists.mpr fun x hx ↦ ne_int z x hx.symm

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