Integer Complement

We define the complement of the integers in the complex plane and give some basic lemmas about it. We also show that the upper half plane embeds into the integer complement.

def Complex.integerComplement : Set ℂ

The complement of the integers in ℂ.

Equations

• Complex.integerComplement = (Set.range Int.cast)ᶜ

theorem Complex.integerComplement_eq : Complex.integerComplement = {z : ℂ | ¬∃ (n : ℤ), ↑n = z}

theorem Complex.integerComplement.mem_iff {x : ℂ} : x ∈ Complex.integerComplement ↔ ¬∃ (n : ℤ), ↑n = x

theorem Complex.UpperHalfPlane.coe_mem_integerComplement (z : UpperHalfPlane) : ↑z ∈ Complex.integerComplement

theorem Complex.integerComplement.add_coe_int_mem {x : ℂ} (a : ℤ) : x + ↑a ∈ Complex.integerComplement ↔ x ∈ Complex.integerComplement

theorem Complex.integerComplement.ne_zero {x : ℂ} (hx : x ∈ Complex.integerComplement) : x ≠ 0

theorem Complex.integerComplement_add_ne_zero {x : ℂ} (hx : x ∈ Complex.integerComplement) (a : ℤ) : x + ↑a ≠ 0

theorem Complex.integerComplement.ne_one {x : ℂ} (hx : x ∈ Complex.integerComplement) : x ≠ 1