isCompact_iff — Mathlib

English

If f is an embedding, then s is compact iff f''s is compact.

Русский

Если f является вложением, то s компактно тогда и только тогда, когда f''s компактно.

LaTeX

$$IsCompact(s) ⇔ IsCompact(f''s)$$

Lean4

/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is compact
if and only if `s` is compact. -/
theorem isCompact_iff {f : X → Y} (hf : IsEmbedding f) : IsCompact s ↔ IsCompact (f '' s) :=
  hf.isInducing.isCompact_iff

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