prod — Mathlib

English

If s and t are separable, then their product s × t is separable.

Русский

Если s и t сепарабельны, то их произведение s × t сепарабельно.

LaTeX

$$$IsSeparable(s) \rightarrow IsSeparable(t) \rightarrow IsSeparable(s \timesˢ t)$$$

Lean4

theorem prod {β : Type*} [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsSeparable s) (ht : IsSeparable t) :
    IsSeparable (s ×ˢ t) := by
  rcases hs with ⟨cs, cs_count, hcs⟩
  rcases ht with ⟨ct, ct_count, hct⟩
  refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩
  rw [closure_prod_eq]
  gcongr

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