instSigmaCompactSpaceProd — Mathlib

English

IsSigmaCompact s is equivalent to SigmaCompactSpace s.

Русский

IsSigmaCompact s эквивалентно SigmaCompactSpace s.

LaTeX

$$$IsSigmaCompact s \\leftrightarrow SigmaCompactSpace s$$$

Lean4

instance [SigmaCompactSpace Y] : SigmaCompactSpace (X × Y) :=
  ⟨⟨fun n => compactCovering X n ×ˢ compactCovering Y n, fun _ =>
      (isCompact_compactCovering _ _).prod (isCompact_compactCovering _ _), by
      simp only [iUnion_prod_of_monotone (compactCovering_subset X) (compactCovering_subset Y), iUnion_compactCovering,
        univ_prod_univ]⟩⟩

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