English
If f is proper and K is compact in Y, then f^{-1}(K) is compact in X.
Русский
Если f правильное отображение и K компактно в Y, то его прообраз по f — компакт в X.
LaTeX
$$$IsProperMap(f) \Rightarrow IsCompact(K) \Rightarrow IsCompact(f^{-1}(K))$$$
Lean4
/-- The preimage of a compact set by a proper map is again compact. See also
`isProperMap_iff_isCompact_preimage` which proves that this property completely characterizes
proper map when the codomain is compactly generated and Hausdorff. -/
theorem isCompact_preimage (h : IsProperMap f) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K) :=
by
rw [isCompact_iff_ultrafilter_le_nhds]
-- Let `𝒰 ≤ 𝓟 (f ⁻¹' K)` an ultrafilter.
intro 𝒰 h𝒰
rw [← comap_principal, ← map_le_iff_le_comap, ← Ultrafilter.coe_map] at h𝒰
rcases hK.ultrafilter_le_nhds _ h𝒰 with
⟨y, hyK, hy⟩
-- Then, by properness of `f`, that means that `𝒰` tends to some `x ∈ f ⁻¹' {y} ⊆ f ⁻¹' K`,
-- which completes the proof.
rcases h.ultrafilter_le_nhds_of_tendsto hy with ⟨x, rfl, hx⟩
exact ⟨x, hyK, hx⟩
