Compact parabolic balls and changes of center

Compactness is transported through the product homeomorphism. The ball inclusion uses the triangle inequality and applies without any positivity assumption on its radii.

theorem CKN.Core.Endgame.isCompact_parabolic_closedBall (z₀ : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : IsCompact (Metric.closedBall z₀ r)

Every closed ball for the parabolic metric is compact.

theorem CKN.Core.Endgame.parabolic_ball_subset_ball_of_center_mem_closedBall {z z₀ : Foundation.Parabolic.ParabolicPoint} {r s R : ℝ} (hz : z ∈ Metric.closedBall z₀ r) (hr : r + s ≤ R) : Metric.ball z s ⊆ Metric.ball z₀ R

A ball around a point of a closed ball stays in the outer ball when the sum of the two radii is at most the outer radius.