The closed upper half-plane in the Riemann sphere

The closure of the open upper half-plane in OnePoint ℂ consists of the finite closed upper half-plane together with infinity. Its approach filter at infinity is the usual cobounded filter restricted to the upper half-plane. These descriptions allow analytic boundary limits in the plane to be assembled into continuous sphere-valued extensions.

theorem TauCeti.nhdsWithin_infty_coe_image_upperHalfPlaneSet : nhdsWithin OnePoint.infty (OnePoint.some '' UpperHalfPlane.upperHalfPlaneSet) = Filter.map OnePoint.some (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet)

Approaching infinity from the upper half-plane in the sphere is equivalent to escaping bounded subsets of the plane within the upper half-plane.

theorem TauCeti.closure_coe_image_upperHalfPlaneSet : closure (OnePoint.some '' UpperHalfPlane.upperHalfPlaneSet) = insert OnePoint.infty (OnePoint.some '' {z : ℂ | 0 ≤ z.im})

The closure of the upper half-plane in the sphere is its finite closed half-plane with the point at infinity added.

theorem TauCeti.ofReal_mem_closure_coe_image_upperHalfPlaneSet (p : ℝ) : ↑↑p ∈ closure (OnePoint.some '' UpperHalfPlane.upperHalfPlaneSet)

Every real point lies in the closure of the upper half-plane in the sphere.