isCompact_iff_isCompact_univ — Mathlib

English

Let X be a topological space and s a subset of X. Then s is compact if and only if the subspace s, endowed with the subspace topology, is compact.

Русский

Пусть X --- топологическое пространство и s ⊆ X. Тогда s компактно тогда и только тогда, когда подпространство s, снабжённое подпространственной топологией, компактно.

LaTeX

$$$\IsCompact(s) \iff \IsCompact(\mathrm{univ} : \mathrm{Set}\,s)$$$

Lean4

theorem isCompact_iff_isCompact_univ : IsCompact s ↔ IsCompact (univ : Set s) := by
  rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]

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