upperHalfPlane_inter_integerComplement

English

The intersection of the open upper half-plane {z ∈ C : Im z > 0} with the integer-complement set equals the upper half-plane, i.e., the integer-complement subset contains the upper half-plane.

Русский

Пересечение открытой верхней полуплоскости {z ∈ ℂ : Im z > 0} с ℂ_ℤ равно верхней полуплоскости.

LaTeX

$$$\{ z \,|\, 0 < \Im(z) \} \cap \mathbb{C}_{\mathbb{Z}} = \{ z \,|\, 0 < \Im(z) \}$$$

Lean4

theorem upperHalfPlane_inter_integerComplement : {z : ℂ | 0 < z.im} ∩ ℂ_ℤ = {z : ℂ | 0 < z.im} :=
  by
  ext z
  simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_iff_left_iff_imp]
  exact fun hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩

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