English
If there exists a sequence of compact closed balls with the same center and radii tending to infinity, the space is proper.
Русский
Если существует последовательность компактных замкнутых шаров с одинаковым центром и радиусы которых стремятся к бесконечности, пространство корректно.
LaTeX
$$$\text{ProperSpace}(\alpha)$ via $\exists (x,r_i)$ with $\overline{B}(x,r_i)$ compact and $r_i \to \infty$$$
Lean4
/-- If there exists a sequence of compact closed balls with the same center
such that the radii tend to infinity, then the space is proper. -/
theorem of_seq_closedBall {β : Type*} {l : Filter β} [NeBot l] {x : α} {r : β → ℝ} (hr : Tendsto r l atTop)
(hc : ∀ᶠ i in l, IsCompact (closedBall x (r i))) : ProperSpace α where
isCompact_closedBall a
r :=
let ⟨_i, hci, hir⟩ := (hc.and <| hr.eventually_ge_atTop <| r + dist a x).exists
hci.of_isClosed_subset isClosed_closedBall <| closedBall_subset_closedBall' hir
