noncompactSpace_left — Mathlib

English

If X is noncompact and Y is nonempty, then X × Y is noncompact.

Русский

Если X некомпактно, а Y непусто, то X × Y некомпактно.

LaTeX

$$$\text{NoncompactSpace}(X) \land \text{Nonempty}(Y) \Rightarrow \text{NoncompactSpace}(X \times Y)$$$

Lean4

instance (priority := 100) noncompactSpace_left [NoncompactSpace X] [Nonempty Y] : NoncompactSpace (X × Y) :=
  Prod.noncompactSpace_iff.2
    (Or.inl ⟨‹_›, ‹_›⟩)
      -- See Note [lower instance priority]

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