English
If each X_i is locally compact and each X_i is locally compact, then the function space ∀ i, X_i is locally compact under appropriate conditions (non-Hausdorff form).
Русский
Если каждое пространство X_i локально компактно, то пространство функций ∀ i, X_i локально компактно (в нехоотражающей форме).
LaTeX
$$$\forall i, TopologicalSpace\;(X_i)\;\wedge\; (LocallyCompactSpace\; (X_i))$ ⇒ LocallyCompactSpace\; (\forall i, X_i)$$
Lean4
/-- For spaces that are not Hausdorff. -/
instance locallyCompactSpace [∀ i, CompactSpace (X i)] : LocallyCompactSpace (∀ i, X i) :=
⟨fun t n hn => by
rw [nhds_pi, Filter.mem_pi] at hn
obtain ⟨s, hs, n', hn', hsub⟩ := hn
choose n'' hn'' hsub' hc using fun i => LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)
refine ⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩
· exact (set_pi_mem_nhds_iff hs _).mpr fun i _ => hn'' i
· exact forall₂_imp fun i _ hi' => hsub' i hi'
·
classical
rw [← Set.univ_pi_ite]
refine isCompact_univ_pi fun i => ?_
by_cases h : i ∈ s
· rw [if_pos h]
exact hc i
· rw [if_neg h]
exact CompactSpace.isCompact_univ⟩
