integerComplement — Mathlib

English

The set ℂ_ℤ is the complement of the set of Gaussian integers within the complex plane.

Русский

Множество ℂ_ℤ есть дополнение множества гауссовых целых внутри плоскости комплексных чисел.

LaTeX

$$$\\text{Complex.integerComplement} = \\mathbb{C} \\setminus \\{ n+mi : n,m \\in \\mathbb{Z} \\}.$$$

Lean4

/-- The complement of the integers in `ℂ` -/
def integerComplement :=
  (Set.range ((↑) : ℤ → ℂ))ᶜ

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