isCompact_iff — Mathlib

English

Sets of a subtype are compact iff the image under the coercion is compact.

Русский

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

LaTeX

$$$IsCompact(s) \iff IsCompact((\\uparrow)''s)$$$

Lean4

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

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