isCompact_preimage' — Mathlib

English

The preimage of a compact set under an inducing map is compact (variant).

Русский

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

LaTeX

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

Lean4

/-- The preimage of a compact set in the image of an inducing map is compact. -/
theorem isCompact_preimage' (hf : IsInducing f) {K : Set Y} (hK : IsCompact K) (Kf : K ⊆ range f) :
    IsCompact (f ⁻¹' K) :=
  (hf.isCompact_preimage_iff Kf).2 hK

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