instSeparableSpaceProd — Mathlib

English

The product of two separable spaces is a separable space.

Русский

Произведение двух разделимых пространств — разделимо.

LaTeX

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

Lean4

/-- The product of two separable spaces is a separable space. -/
instance [TopologicalSpace β] [SeparableSpace α] [SeparableSpace β] : SeparableSpace (α × β) :=
  by
  rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
  rcases exists_countable_dense β with ⟨t, htc, htd⟩
  exact ⟨⟨s ×ˢ t, hsc.prod htc, hsd.prod htd⟩⟩

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