isSigmaCompact_iff — Mathlib

English

A set of the subtype is σ-compact iff its image under the coercion into the ambient space is σ-compact.

Русский

Множество подтипа σ-компактно тогда и только тогда, когда его образ под приведением в надмножество σ-компактен.

LaTeX

$$$IsSigmaCompact s \\leftrightarrow IsSigmaCompact ((↑) '' s)$$$

Lean4

/-- Sets of subtype are σ-compact iff the image under a coercion is. -/
theorem isSigmaCompact_iff {p : X → Prop} {s : Set { a // p a }} :
    IsSigmaCompact s ↔ IsSigmaCompact ((↑) '' s : Set X) :=
  IsEmbedding.subtypeVal.isSigmaCompact_iff

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