isCompact_preimage_iff — Mathlib

English

For an inducing map f, and K ⊆ range f, IsCompact (f⁻¹'(K)) ⇔ IsCompact(K).

Русский

Для индуктивного отображения f и K ⊆ range f выполняется: компактность обратного образа ⇔ компактность K.

LaTeX

$$IsCompact(f⁻¹'(K)) ⇔ IsCompact(K) (when hf : IsInducing f and K ⊆ range f)$$

Lean4

theorem isCompact_preimage_iff {f : X → Y} (hf : IsInducing f) {K : Set Y} (Kf : K ⊆ range f) :
    IsCompact (f ⁻¹' K) ↔ IsCompact K := by rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]

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