instNoncompactSpace — Mathlib

English

The upper-half-plane ℍ is noncompact.

Русский

Верхняя полуплоскость ℍ не компактна.

LaTeX

$$$\\\\mathbb{H}$ is noncompact.$$

Lean4

instance : NoncompactSpace ℍ := by
  refine ⟨fun h => ?_⟩
  have : IsCompact (Complex.im ⁻¹' Ioi 0) := isCompact_iff_isCompact_univ.2 h
  replace := this.isClosed.closure_eq
  rw [closure_preimage_im, closure_Ioi, Set.ext_iff] at this
  exact absurd ((this 0).1 (@left_mem_Ici ℝ _ 0)) (@lt_irrefl ℝ _ 0)

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