integerComplement_eq

Mathlib.Analysis.Complex.IntegerCompl

URI: https://scilib.ai/kg/mathlib#Complex.integerComplement_eq

English

The symbol ℂ_ℤ equals the set {z ∈ ℂ : not exists n ∈ ℤ with n = z}.

Русский

Обозначение ℂ_ℤ равно {z ∈ ℂ : не существует n ∈ ℤ, такого, что n = z}.

LaTeX

$$$\\mathbb{C}_{\\mathbb{Z}} = \\{ z \\in \\mathbb{C} : \\neg \\exists n \\in \\mathbb{Z}, n = z \\}.$$$

Lean4

theorem integerComplement_eq : ℂ_ℤ = {z : ℂ | ¬∃ (n : ℤ), n = z} :=
  rfl

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

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

Разделы

Аффилиация

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