prod_properSpace — Mathlib

English

A binary product of proper metric spaces is a proper space.

Русский

Двоичное произведение правильных метрических пространств является правильным пространством.

LaTeX

$$$\\text{ProperSpace}(\\alpha) \\land \\text{ProperSpace}(\\beta) \\Rightarrow \\text{ProperSpace}(\\alpha \\times \\beta)$$$

Lean4

/-- A binary product of proper spaces is proper. -/
instance prod_properSpace {α : Type*} {β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [ProperSpace α]
    [ProperSpace β] : ProperSpace (α × β) where
  isCompact_closedBall := by
    rintro ⟨x, y⟩ r
    rw [← closedBall_prod_same x y]
    exact (isCompact_closedBall x r).prod (isCompact_closedBall y r)

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