isSigmaCompact_iff — Mathlib

English

If f is an embedding, then s is σ-compact iff f(s) is σ-compact.

Русский

Если f — вложение, то s σ-компактно тогда и только тогда, когда f(s) σ-компактно.

LaTeX

$$$IsEmbedding f \\rightarrow (IsSigmaCompact s \\leftrightarrow IsSigmaCompact (f''s))$$$

Lean4

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

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