instProperSpace — Mathlib

English

The distance on ℕ+ is the same as the distance on the underlying ℕ when viewed through the inclusion; i.e., dist(↑x,↑y) = dist(x,y).

Русский

Расстояние на ℕ+ совпадает с расстоянием между соответствующими элементами в ℕ через вложение; dist(↑x,↑y) = dist(x,y).

LaTeX

$$$\operatorname{dist}(\uparrow x, \uparrow y) = \operatorname{dist}(x,y)$$$

Lean4

instance : ProperSpace ℕ+ where
  isCompact_closedBall n
    r := by
    change IsCompact (((↑) : ℕ+ → ℕ) ⁻¹' closedBall (↑n : ℕ) r)
    rw [Nat.closedBall_eq_Icc]
    exact ((Set.finite_Icc _ _).preimage PNat.coe_injective.injOn).isCompact

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