of_isCompact_closedBall_of_le — Mathlib

English

If all sufficiently large closed balls are compact, the space is proper.

Русский

Если все достаточно большие замкнутые шары компактны, пространство является правильным.

LaTeX

$$$\text{ProperSpace}(\alpha)$ if $\forall R, (\forall x,r, R \le r \Rightarrow IsCompact(\overline{B}(x,r)))$$$

Lean4

/-- If all closed balls of large enough radius are compact, then the space is proper. Especially
useful when the lower bound for the radius is 0. -/
theorem of_isCompact_closedBall_of_le (R : ℝ) (h : ∀ x : α, ∀ r, R ≤ r → IsCompact (closedBall x r)) : ProperSpace α :=
  ⟨fun x r =>
    IsCompact.of_isClosed_subset (h x (max r R) (le_max_right _ _)) isClosed_closedBall
      (closedBall_subset_closedBall <| le_max_left _ _)⟩

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