pi_properSpace — Mathlib

English

A finite product of proper spaces is a proper space.

Русский

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

LaTeX

$$$\\forall b, \\text{ProperSpace}(X(b)) \\Rightarrow \\text{ProperSpace}(\\prod_{b\\in \\beta} X(b))$$$

Lean4

/-- A finite product of proper spaces is proper. -/
instance pi_properSpace {X : β → Type*} [Fintype β] [∀ b, PseudoMetricSpace (X b)] [h : ∀ b, ProperSpace (X b)] :
    ProperSpace (∀ b, X b) := by
  refine .of_isCompact_closedBall_of_le 0 fun x r hr => ?_
  rw [closedBall_pi _ hr]
  exact isCompact_univ_pi fun _ => isCompact_closedBall _ _

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