English
A map is proper if and only if it is continuous and ultrafilter criterion holds: for every ultrafilter 𝒰 on X and every y in Y, Tendsto f 𝒰 (nhds y) implies there exists x with f x = y and 𝒰 ≤ nhds x.
Русский
Пусть f: X→Y; тогда f проперна тогда и только тогда, когда она непрерывна и для любого ультрафильтра 𝒰 на X и любого y∈Y, Tendsto f 𝒰 (nhds y) эквивалентно существованию x с f x = y и 𝒰 ≤ nhds x.
LaTeX
$$$IsProperMap(f) \iff (Continuous(f) \land \forall 𝒰\!:\!Ultrafilter X, \forall y:\!Y, Tendsto f 𝒰 (nhds y) \rightarrow \exists x, f(x)=y \land 𝒰 \le nhds x)$$$
Lean4
/-- Characterization of proper maps by ultrafilters. -/
theorem isProperMap_iff_ultrafilter :
IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄, ∀ ⦃y : Y⦄, Tendsto f 𝒰 (𝓝 y) → ∃ x, f x = y ∧ 𝒰 ≤ 𝓝 x := by
-- This is morally trivial since ultrafilters give all the information about cluster points.
rw [isProperMap_iff_clusterPt]
refine and_congr_right (fun _ ↦ ?_)
constructor <;> intro H
· intro 𝒰 y (hY : (Ultrafilter.map f 𝒰 : Filter Y) ≤ _)
simp_rw [← Ultrafilter.clusterPt_iff] at hY ⊢
exact H hY
· simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, ← exists_ultrafilter_iff, forall_exists_index]
intro ℱ y 𝒰 hy
rcases H (tendsto_iff_comap.mpr <| hy.trans inf_le_left) with ⟨x, hxy, hx⟩
exact ⟨x, hxy, 𝒰, le_inf hx (hy.trans inf_le_right)⟩
