English
A map f is proper if and only if it is continuous and tends to cocompact: Tendsto f (cocompact X) (cocompact Y).
Русский
Отображение пропорно тогда и только тогда, когда оно непрерывно и стремится к кокомпактности: Tendsto f (cocompact X) (cocompact Y).
LaTeX
$$$IsProperMap(f) \\iff (Continuous(f) \\land Tendsto\\,f\\, (cocompact\\,X) (cocompact\\,Y))$$$
Lean4
/-- Version of `isProperMap_iff_isCompact_preimage` in terms of `cocompact`.
There was an older version of this theorem which was changed to this one to make use
of the `CompactlyGeneratedSpace` typeclass. (since 2024-11-10) -/
theorem isProperMap_iff_tendsto_cocompact : IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y) :=
by
simp_rw [isProperMap_iff_isCompact_preimage, hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set,
preimage_compl]
refine and_congr_right fun f_cont ↦ ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩
rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩
exact hK'.of_isClosed_subset (hK.isClosed.preimage f_cont) (compl_le_compl_iff_le.mp hK'y)
