instCompactSpaceSum — Mathlib

English

The disjoint sum (coproduct) of two compact spaces is compact.

Русский

Дискретное объединение двух компактных пространств компактно.

LaTeX

$$$\text{CompactSpace}(X) \land \text{CompactSpace}(Y) \Rightarrow \text{CompactSpace}(X \oplus Y)$$$

Lean4

/-- The disjoint union of two compact spaces is compact. -/
instance [CompactSpace X] [CompactSpace Y] : CompactSpace (X ⊕ Y) :=
  ⟨by
    rw [← range_inl_union_range_inr]
    exact (isCompact_range continuous_inl).union (isCompact_range continuous_inr)⟩

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