isCompact_preimage — Mathlib

English

The preimage of a compact set under a closed embedding is compact.

Русский

Обратный образ компактного множества по замкнутому вложению компактный.

LaTeX

$$IsCompact (f⁻¹'(K))$$

Lean4

/-- The preimage of a compact set under a closed embedding is a compact set. -/
theorem isCompact_preimage (hf : IsClosedEmbedding f) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K) :=
  hf.isInducing.isCompact_preimage (hf.isClosed_range) hK

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