noncompactSpace_iff — Mathlib

English

NoncompactSpace (X × Y) is equivalent to (NoncompactSpace X ∧ Nonempty Y) or (Nonempty X ∧ NoncompactSpace Y).

Русский

Некопакстпность произведения равна либо некомпактности X вместе с непустотой Y, либо не пустоте X и некомпактности Y.

LaTeX

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

Lean4

theorem noncompactSpace_iff :
    NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y := by
  simp [← Filter.cocompact_neBot_iff, ← Filter.coprod_cocompact, Filter.coprod_neBot_iff]
    -- See Note [lower instance priority]

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