English
If f is a topology-inducing map with locally closed range, then the domain is locally compact.
Русский
Если отображение является индуцирующим топологию и образ локально замкнут, то область определения локально компактна.
LaTeX
$$$[LocallyCompactSpace\;Y]\ {f:X\to Y}, IsInducing\;f \rightarrow IsLocallyClosed\;(range\;f) \rightarrow LocallyCompactSpace\;X$$$
Lean4
/-- If `f` is a topology inducing map with a locally compact codomain and a locally closed range,
then the domain of `f` is a locally compact space. -/
theorem locallyCompactSpace [LocallyCompactSpace Y] {f : X → Y} (hf : IsInducing f) (h : IsLocallyClosed (range f)) :
LocallyCompactSpace X := by
rcases h with ⟨U, Z, hU, hZ, hUZ⟩
have (x : X) : (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) (fun s ↦ f ⁻¹' (s ∩ Z)) :=
by
have H : U ∈ 𝓝 (f x) := hU.mem_nhds (hUZ.subset <| mem_range_self _).1
rw [hf.nhds_eq_comap, ← comap_nhdsWithin_range, hUZ, nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)]
exact (nhdsWithin_hasBasis ((compact_basis_nhds (f x)).restrict_subset H) _).comap _
refine .of_hasBasis this fun x s ⟨⟨_, hs⟩, hsU⟩ ↦ ?_
rw [hf.isCompact_preimage_iff]
exacts [hs.inter_right hZ, hUZ ▸ by gcongr]
